src/HOL/Set.ML
changeset 9422 4b6bc2b347e5
parent 9378 12f251a5a3b5
child 9687 772ac061bd76
     1.1 --- a/src/HOL/Set.ML	Mon Jul 24 23:51:11 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Jul 24 23:51:46 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/set
     1.5 +(*  Title:      HOL/Set.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9 @@ -719,9 +719,9 @@
    1.10  (*Split ifs on either side of the membership relation.
    1.11  	Not for Addsimps -- can cause goals to blow up!*)
    1.12  bind_thm ("split_if_mem1", 
    1.13 -    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
    1.14 +    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
    1.15  bind_thm ("split_if_mem2", 
    1.16 -    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    1.17 +    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
    1.18  
    1.19  bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    1.20  		  split_if_mem1, split_if_mem2]);