src/HOL/Set.ML
changeset 6394 3d9fd50fcc43
parent 6301 08245f5a436d
child 6443 6d5d3ecedf50
     1.1 --- a/src/HOL/Set.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -656,9 +656,9 @@
     1.4  (*Split ifs on either side of the membership relation.
     1.5  	Not for Addsimps -- can cause goals to blow up!*)
     1.6  bind_thm ("split_if_mem1", 
     1.7 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
     1.8 +    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
     1.9  bind_thm ("split_if_mem2", 
    1.10 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    1.11 +    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    1.12  
    1.13  val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    1.14  		  split_if_mem1, split_if_mem2];