qualified MetaSimplifier.norm_hhf(_protect);

--- a/src/Pure/Isar/element.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -245,7 +245,7 @@
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
-    val th = norm_hhf raw_th;
+    val th = MetaSimplifier.norm_hhf raw_th;
     val is_elim = ObjectLogic.is_elim th;
 
     val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
@@ -291,7 +291,7 @@
   Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     Tactic.rtac Drule.protectI 1 THEN tac));
 
-fun conclude_witness (Witness (_, th)) = norm_hhf (Goal.conclude th);
+fun conclude_witness (Witness (_, th)) = MetaSimplifier.norm_hhf_protect (Goal.conclude th);
 
 val mark_witness = Logic.protect;
 

--- a/src/Pure/Isar/obtain.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -187,7 +187,7 @@
     val rule =
       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
-      | SOME th => check_result ctxt thesis (norm_hhf (Goal.conclude th)));
+      | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
 
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
@@ -292,7 +292,7 @@
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
       ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
-    val before_qed = SOME (Method.primitive_text (Goal.conclude #> norm_hhf #>
+    val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
       Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;

--- a/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -47,7 +47,7 @@
 *)
 fun presume_export _ = assume_export false;
 
-val assume = norm_hhf o Thm.assume;
+val assume = MetaSimplifier.norm_hhf o Thm.assume;
 
 
 
@@ -100,9 +100,9 @@
 
 fun export is_goal inner outer =
   let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
-    norm_hhf_protect
+    MetaSimplifier.norm_hhf_protect
     #> fold_rev (fn (e, As) => e is_goal As) asms
-    #> norm_hhf_protect
+    #> MetaSimplifier.norm_hhf_protect
   end;
 
 fun export_morphism inner outer =

--- a/src/Pure/meta_simplifier.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -72,8 +72,6 @@
   val addSSolver: simpset * solver -> simpset
   val setSolver: simpset * solver -> simpset
   val addSolver: simpset * solver -> simpset
-  val norm_hhf: thm -> thm
-  val norm_hhf_protect: thm -> thm
 end;
 
 signature META_SIMPLIFIER =
@@ -104,6 +102,8 @@
   val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_goal_rule: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
+  val norm_hhf: thm -> thm
+  val norm_hhf_protect: thm -> thm
 end;
 
 structure MetaSimplifier: META_SIMPLIFIER =

--- a/src/Pure/subgoal.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/subgoal.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -29,7 +29,8 @@
 
 fun focus ctxt i st =
   let
-    val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
+    val ((schematics, [st']), ctxt') =
+      Variable.import true [MetaSimplifier.norm_hhf_protect st] ctxt;
     val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
     val asms = Drule.strip_imp_prems goal;
     val concl = Drule.strip_imp_concl goal;