--- a/src/HOL/Set.ML Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Set.ML Fri Sep 15 12:39:57 2000 +0200
@@ -720,13 +720,11 @@
(*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 (the_context ())) [("P", "%x. x : ?b")] split_if);
-bind_thm ("split_if_mem2",
- read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
+bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
+bind_thm ("split_if_mem2", inst "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]);
+ split_if_mem1, split_if_mem2]);
(*Each of these has ALREADY been added to simpset() above.*)