# HG changeset patch
# User wenzelm
# Date 1154000586 -7200
# Node ID e0f9e8a6556b0e71cad004c7d56598db529887b7
# Parent  435601e8e53da3bfb13de0356286b19e171c9310
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

diff -r 435601e8e53d -r e0f9e8a6556b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Jul 27 13:43:05 2006 +0200
+++ b/src/Pure/goal.ML	Thu Jul 27 13:43:06 2006 +0200
@@ -17,8 +17,6 @@
   val protect: thm -> thm
   val conclude: thm -> thm
   val finish: thm -> thm
-  val norm_hhf: thm -> thm
-  val norm_hhf_protect: thm -> thm
   val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
   val comp_hhf: thm -> thm -> thm
@@ -76,28 +74,6 @@
 
 (** results **)
 
-(* HHF normal form: !! before ==>, outermost !! generalized *)
-
-local
-
-fun gen_norm_hhf ss =
-  (not o Drule.is_norm_hhf o Thm.prop_of) ?
-    Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) ss)
-  #> Thm.adjust_maxidx_thm
-  #> Drule.gen_all;
-
-val ss =
-  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
-    addsimps [Drule.norm_hhf_eq];
-
-in
-
-val norm_hhf = gen_norm_hhf ss;
-val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
-
-end;
-
-
 (* composition of normal results *)
 
 fun compose_hhf tha i thb =
diff -r 435601e8e53d -r e0f9e8a6556b src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Jul 27 13:43:05 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 27 13:43:06 2006 +0200
@@ -72,6 +72,8 @@
   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 =
@@ -1200,6 +1202,26 @@
   then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
   else raise THM("rewrite_goal_rule",i,[thm]);
 
+
+(* HHF normal form: !! before ==>, outermost !! generalized *)
+
+local
+
+fun gen_norm_hhf ss =
+  (not o Drule.is_norm_hhf o Thm.prop_of) ?
+    Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
+  #> Thm.adjust_maxidx_thm
+  #> Drule.gen_all;
+
+val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
+
+in
+
+val norm_hhf = gen_norm_hhf ss;
+val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
+
+end;
+
 end;
 
 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;