stay within regular tactic language -- avoid operating on whole proof state;

--- 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;