stay within regular tactic language -- avoid operating on whole proof state;
authorwenzelm
Thu May 30 12:56:25 2013 +0200 (2013-05-30)
changeset 52231cc30c4eb4ec9
parent 52230 1105b3b5aa77
child 52232 a2d4ae3e04a2
stay within regular tactic language -- avoid operating on whole proof state;
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu May 30 12:35:40 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu May 30 12:56:25 2013 +0200
     1.3 @@ -141,7 +141,7 @@
     1.4        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
     1.5      EVERY [REPEAT_DETERM_N r
     1.6          (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
     1.7 -      if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
     1.8 +      if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, atac 1,
     1.9        mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs]
    1.10    end;
    1.11