--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 16 19:40:03 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 16 23:36:55 2009 +0100
@@ -807,12 +807,12 @@
text %mlref {*
\begin{mldecls}
- @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\
+ @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{ML MetaSimplifier.norm_hhf}~@{text thm} normalizes the given
+ \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given
theorem according to the canonical form specified above. This is
occasionally helpful to repair some low-level tools that do not
handle Hereditary Harrop Formulae properly.
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 16 19:40:03 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 16 23:36:55 2009 +0100
@@ -821,12 +821,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
+ \indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\
\end{mldecls}
\begin{description}
- \item \verb|MetaSimplifier.norm_hhf|~\isa{thm} normalizes the given
+ \item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given
theorem according to the canonical form specified above. This is
occasionally helpful to repair some low-level tools that do not
handle Hereditary Harrop Formulae properly.
--- a/src/HOL/Tools/inductive_package.ML Mon Mar 16 19:40:03 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Mar 16 23:36:55 2009 +0100
@@ -302,7 +302,7 @@
hol_simplify inductive_conj
#> hol_simplify inductive_rulify
#> hol_simplify inductive_rulify_fallback
- #> MetaSimplifier.norm_hhf;
+ #> Simplifier.norm_hhf;
end;
--- a/src/Pure/meta_simplifier.ML Mon Mar 16 19:40:03 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Mon Mar 16 23:36:55 2009 +0100
@@ -73,6 +73,8 @@
val prune_params_tac: tactic
val fold_rule: thm list -> thm -> thm
val fold_goals_tac: thm list -> tactic
+ val norm_hhf: thm -> thm
+ val norm_hhf_protect: thm -> thm
end;
signature META_SIMPLIFIER =
@@ -122,8 +124,6 @@
(simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
val asm_rewrite_goal_tac: bool * bool * bool ->
(simpset -> tactic) -> simpset -> int -> tactic
- val norm_hhf: thm -> thm
- val norm_hhf_protect: thm -> thm
val rewrite: bool -> thm list -> conv
val simplify: bool -> thm list -> thm -> thm
end;
--- a/src/Pure/subgoal.ML Mon Mar 16 19:40:03 2009 +0100
+++ b/src/Pure/subgoal.ML Mon Mar 16 23:36:55 2009 +0100
@@ -29,7 +29,7 @@
fun focus ctxt i st =
let
val ((schematics, [st']), ctxt') =
- Variable.import_thms true [MetaSimplifier.norm_hhf_protect st] ctxt;
+ Variable.import_thms true [Simplifier.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;
--- a/src/Tools/coherent.ML Mon Mar 16 19:40:03 2009 +0100
+++ b/src/Tools/coherent.ML Mon Mar 16 23:36:55 2009 +0100
@@ -51,7 +51,7 @@
end;
-fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
+fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
(* Decompose elimination rule of the form
A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P