--- a/src/HOL/Set.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Set.ML Mon Jul 24 23:51:46 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/set
+(* Title: HOL/Set.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -719,9 +719,9 @@
(*Split ifs on either side of the membership relation.
Not for Addsimps -- can cause goals to blow up!*)
bind_thm ("split_if_mem1",
- read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
+ read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
bind_thm ("split_if_mem2",
- read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
+ read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
split_if_mem1, split_if_mem2]);