# HG changeset patch
# User wenzelm
# Date 1230849109 -3600
# Node ID eb782d1dc07ca40effb9c2fbf35de74a955a3573
# Parent  2b845381ba6ae91712d01b7313e5f139b913a3ca
normalized some ML type/val aliases;

diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -5,23 +5,20 @@
 signature DISTINCT_TREE_PROVER =
 sig
   datatype Direction = Left | Right
-  val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
-  val dest_tree : Term.term -> Term.term list
-  val find_tree :
-       Term.term -> Term.term -> Direction list option 
+  val mk_tree : ('a -> term) -> typ -> 'a list -> term
+  val dest_tree : term -> term list
+  val find_tree : term -> term -> Direction list option 
 
-  val neq_to_eq_False : Thm.thm
-  val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
-  val neq_x_y :
-       Proof.context -> Term.term -> Term.term -> string -> Thm.thm option   
-  val distinctFieldSolver : string list -> MetaSimplifier.solver
-  val distinctTree_tac :
-       string list -> Proof.context -> Term.term * int -> Tactical.tactic
-  val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
-  val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
-  val distinct_simproc : string list -> MetaSimplifier.simproc
+  val neq_to_eq_False : thm
+  val distinctTreeProver : thm -> Direction list -> Direction list -> thm
+  val neq_x_y : Proof.context -> term -> term -> string -> thm option   
+  val distinctFieldSolver : string list -> solver
+  val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
+  val distinct_implProver : thm -> cterm -> thm
+  val subtractProver : term -> cterm -> thm -> thm
+  val distinct_simproc : string list -> simproc
   
-  val discharge : Thm.thm list -> Thm.thm -> Thm.thm
+  val discharge : thm list -> thm -> thm
 end;
 
 structure DistinctTreeProver : DISTINCT_TREE_PROVER =
diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Statespace/state_fun.ML
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -8,17 +7,17 @@
   val lookupN : string
   val updateN : string
 
-  val mk_constr : Context.theory -> Term.typ -> Term.term
-  val mk_destr : Context.theory -> Term.typ -> Term.term
+  val mk_constr : theory -> typ -> term
+  val mk_destr : theory -> typ -> term
 
-  val lookup_simproc : MetaSimplifier.simproc
-  val update_simproc : MetaSimplifier.simproc
-  val ex_lookup_eq_simproc : MetaSimplifier.simproc
-  val ex_lookup_ss : MetaSimplifier.simpset
-  val lazy_conj_simproc : MetaSimplifier.simproc
-  val string_eq_simp_tac : int -> Tactical.tactic
+  val lookup_simproc : simproc
+  val update_simproc : simproc
+  val ex_lookup_eq_simproc : simproc
+  val ex_lookup_ss : simpset
+  val lazy_conj_simproc : simproc
+  val string_eq_simp_tac : int -> tactic
 
-  val setup : Context.theory -> Context.theory
+  val setup : theory -> theory
 end;
 
 structure StateFun: STATE_FUN = 
diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -674,7 +674,7 @@
      fun prover used ss thm =
      let fun cong_prover ss thm =
          let val dummy = say "cong_prover:"
-             val cntxt = MetaSimplifier.prems_of_ss ss
+             val cntxt = Simplifier.prems_of_ss ss
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm thm)
@@ -687,7 +687,7 @@
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
-                     val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
+                     val ss' = Simplifier.add_prems (map ASSUME ants) ss
                      val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
                        handle U.ERR _ => Thm.reflexive lhs
                      val dummy = print_thms "proven:" [lhs_eq_lhs1]
@@ -708,7 +708,7 @@
                   val Q = get_lhs eq1
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
-                  val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
+                  val ss' = Simplifier.add_prems (map ASSUME ants1) ss
                   val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
                                 handle U.ERR _ => Thm.reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
@@ -758,7 +758,7 @@
 
         fun restrict_prover ss thm =
           let val dummy = say "restrict_prover:"
-              val cntxt = rev(MetaSimplifier.prems_of_ss ss)
+              val cntxt = rev(Simplifier.prems_of_ss ss)
               val dummy = print_thms "cntxt:" cntxt
               val thy = Thm.theory_of_thm thm
               val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/arith_data.ML
-    ID:         $Id$
     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
 
 Basic arithmetic proof tools.
@@ -7,9 +6,8 @@
 
 signature ARITH_DATA =
 sig
-  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
-    -> MetaSimplifier.simpset -> term * term -> thm
-  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
+  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
+  val simp_all_tac: thm list -> simpset -> tactic
 
   val mk_sum: term list -> term
   val mk_norm_sum: term list -> term
diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -413,7 +413,7 @@
     val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
     val ctxt = ProofContext.init thy;
     val simpset = Simplifier.context ctxt
-      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
+      (Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     val cos = map (fn (co, tys) =>
         (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
     val tac = ALLGOALS (simp_tac simpset)
diff -r 2b845381ba6a -r eb782d1dc07c src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/function_package/fundef_lib.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions. 
@@ -163,7 +162,7 @@
           else if js = []
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
-     (K (MetaSimplifier.rewrite_goals_tac ac
+     (K (rewrite_goals_tac ac
          THEN rtac Drule.reflexive_thm 1))
  end
 
diff -r 2b845381ba6a -r eb782d1dc07c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/Pure/Isar/code.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/code.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Abstract executable content of theory.  Management of data dependent on
@@ -16,8 +15,8 @@
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
-  val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
-  val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
+  val map_pre: (simpset -> simpset) -> theory -> theory
+  val map_post: (simpset -> simpset) -> theory -> theory
   val add_inline: thm -> theory -> theory
   val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
   val del_functrans: string -> theory -> theory
@@ -186,8 +185,8 @@
 (* pre- and postprocessor *)
 
 datatype thmproc = Thmproc of {
-  pre: MetaSimplifier.simpset,
-  post: MetaSimplifier.simpset,
+  pre: simpset,
+  post: simpset,
   functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
 };
 
@@ -198,8 +197,8 @@
 fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
   Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
     let
-      val pre = MetaSimplifier.merge_ss (pre1, pre2);
-      val post = MetaSimplifier.merge_ss (post1, post2);
+      val pre = Simplifier.merge_ss (pre1, pre2);
+      val post = Simplifier.merge_ss (post1, post2);
       val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
     in mk_thmproc ((pre, post), functrans) end;
 
@@ -221,7 +220,7 @@
     val thmproc = merge_thmproc (thmproc1, thmproc2);
     val spec = merge_spec (spec1, spec2);
   in mk_exec (thmproc, spec) end;
-val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []),
+val empty_exec = mk_exec (mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []),
   mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty))));
 
 fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
@@ -417,12 +416,12 @@
       Pretty.block [
         Pretty.str "preprocessing simpset:",
         Pretty.fbrk,
-        MetaSimplifier.pretty_ss pre
+        Simplifier.pretty_ss pre
       ],
       Pretty.block [
         Pretty.str "postprocessing simpset:",
         Pretty.fbrk,
-        MetaSimplifier.pretty_ss post
+        Simplifier.pretty_ss post
       ],
       Pretty.block (
         Pretty.str "function transformers:"
diff -r 2b845381ba6a -r eb782d1dc07c src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -165,7 +165,7 @@
 fun filter_simp ctxt t (_, thm) =
   let
     val (_, {mk_rews = {mk, ...}, ...}) =
-      MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
+      Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
     val extract_simp =
       (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
     val ss = is_matching_thm extract_simp ctxt false t thm
diff -r 2b845381ba6a -r eb782d1dc07c src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -249,7 +249,7 @@
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy1 [] [] t
         (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
-    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+    handle Simplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";