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