Use ASM_SIMP_TAC in UNBETA_TAC

binghe · Dec 5, 2024 · 938e4eb · 938e4eb
1 parent a0cae9d
commit 938e4eb
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/examples/lambda/barendregt/head_reductionLib.sml b/examples/lambda/barendregt/head_reductionLib.sml
@@ -57,13 +57,13 @@ val T_TAC = rpt (Q.PAT_X_ASSUM ‘T’ K_TAC);
    (which eliminates LET and creates abbreviations) but does not do STRIP_TAC
    on the goal.
  *)
-fun UNBETA_TAC ths tm =
-  let val P = genvar (type_of tm --> bool)
-  in
+fun UNBETA_TAC ths tm = let
+    val P = genvar (type_of tm --> bool)
+in
     CONV_TAC (UNBETA_CONV tm)
  >> qmatch_abbrev_tac ‘^P _’
  >> RW_TAC bool_ss ths
- >> simp [Abbr ‘^P’]
-  end;
+ >> ASM_SIMP_TAC std_ss [Abbr ‘^P’]
+end;
 
 end (* struct *)