# HG changeset patch
# User wenzelm
# Date 1005844898 -3600
# Node ID 09bc6f8456b99c63ed2d4f9f1043891e2dd16b9a
# Parent  5efe7b6874fd8895965f7846408ef16899f8cb09
type_solver_tac: use TCSET' to refer to context of goal state (does
  *not* work with local proof contexts of Isar / new-style locales);

diff -r 5efe7b6874fd -r 09bc6f8456b9 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Nov 15 18:20:48 2001 +0100
+++ b/src/ZF/simpdata.ML	Thu Nov 15 18:21:38 2001 +0100
@@ -45,10 +45,12 @@
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
-                           addcongs [if_weak_cong]
-		           addsplits [split_if]
-                           setSolver (mk_solver "types" Type_solver_tac);
+simpset_ref() :=
+  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
+  addcongs [if_weak_cong]
+  addsplits [split_if]
+  setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
+
 
 (** Splitting IFs in the assumptions **)