# HG changeset patch
# User wenzelm
# Date 1129583424 -7200
# Node ID 9a4aea3a9ae1117ed73c5c0a40b96ebdcf3b186e
# Parent  a1f797ff091e237c163d5c3d5e334c690646eb1f
added type_solver (uses Simplifier.the_context);
removed obsolete context_type_solver;

diff -r a1f797ff091e -r 9a4aea3a9ae1 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Mon Oct 17 23:10:23 2005 +0200
+++ b/src/ZF/Tools/typechk.ML	Mon Oct 17 23:10:24 2005 +0200
@@ -31,7 +31,7 @@
   val Typecheck_tac: tactic
   val Type_solver_tac: thm list -> int -> tactic
   val local_tcset_of: Proof.context -> tcset
-  val context_type_solver: context_solver
+  val type_solver: solver
 end;
 
 signature TYPE_CHECK =
@@ -174,8 +174,8 @@
 
 (* solver *)
 
-val context_type_solver =
-  Simplifier.mk_context_solver "context types" (type_solver_tac o local_tcset_of);
+val type_solver = Simplifier.mk_solver' "ZF types" (fn ss =>
+  type_solver_tac (local_tcset_of (Simplifier.the_context ss)) (Simplifier.prems_of_ss ss));
 
 
 (* attributes *)
@@ -211,7 +211,7 @@
 
 val setup =
  [TypecheckingData.init, LocalTypecheckingData.init,
-  Simplifier.add_context_unsafe_solver context_type_solver,
+  fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy),
   Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
   Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];