# HG changeset patch
# User wenzelm
# Date 1237243015 -3600
# Node ID 58db562784787dfb56e73b33e85926486ab37a9e
# Parent  24e156db414c0c35dace32bd0d544ab20bc5c593
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;

diff -r 24e156db414c -r 58db56278478 doc-src/IsarImplementation/Thy/Logic.thy
--- 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.
diff -r 24e156db414c -r 58db56278478 doc-src/IsarImplementation/Thy/document/Logic.tex
--- 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.
diff -r 24e156db414c -r 58db56278478 src/HOL/Tools/inductive_package.ML
--- 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;
 
diff -r 24e156db414c -r 58db56278478 src/Pure/meta_simplifier.ML
--- 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;
diff -r 24e156db414c -r 58db56278478 src/Pure/subgoal.ML
--- 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;
diff -r 24e156db414c -r 58db56278478 src/Tools/coherent.ML
--- 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