--- a/src/ZF/Tools/typechk.ML Thu Nov 15 18:09:40 2001 +0100
+++ b/src/ZF/Tools/typechk.ML Thu Nov 15 18:15:13 2001 +0100
@@ -20,6 +20,8 @@
val tcset_ref_of: theory -> tcset ref
val tcset_of: theory -> tcset
val tcset: unit -> tcset
+ val TCSET: (tcset -> tactic) -> tactic
+ val TCSET': (tcset -> 'a -> tactic) -> 'a -> tactic
val AddTCs: thm list -> unit
val DelTCs: thm list -> unit
val TC_add_global: theory attribute
@@ -146,6 +148,9 @@
val tcset = tcset_of o Context.the_context;
val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
+fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
+fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
+
(* change global tcset *)