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