# HG changeset patch
# User wenzelm
# Date 1369911385 -7200
# Node ID cc30c4eb4ec93127d808b7f66769f067bedb63e9
# Parent  1105b3b5aa77345eb246fc9a6010b62b6f0299de
stay within regular tactic language -- avoid operating on whole proof state;

diff -r 1105b3b5aa77 -r cc30c4eb4ec9 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu May 30 12:35:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu May 30 12:56:25 2013 +0200
@@ -141,7 +141,7 @@
       REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
     EVERY [REPEAT_DETERM_N r
         (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
-      if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
+      if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, atac 1,
       mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs]
   end;