--- a/src/ZF/QPair.ML Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/QPair.ML Mon Nov 03 12:24:13 1997 +0100
@@ -85,7 +85,7 @@
qed_goalw "QSigma_cong" thy [QSigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ QSigma(A,B) = QSigma(A',B')"
- (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
+ (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
(fn _ => [ (Blast_tac 1) ]);
@@ -100,11 +100,11 @@
qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
(fn _=>
- [ (blast_tac (!claset addIs [the_equality]) 1) ]);
+ [ (blast_tac (claset() addIs [the_equality]) 1) ]);
qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
(fn _=>
- [ (blast_tac (!claset addIs [the_equality]) 1) ]);
+ [ (blast_tac (claset() addIs [the_equality]) 1) ]);
Addsimps [qfst_conv, qsnd_conv];
@@ -137,7 +137,7 @@
\ |] ==> qsplit(%x y. c(x,y), p) : C(p)"
(fn major::prems=>
[ (rtac (major RS QSigmaE) 1),
- (asm_simp_tac (!simpset addsimps prems) 1) ]);
+ (asm_simp_tac (simpset() addsimps prems) 1) ]);
goalw thy [qsplit_def]
"!!u. u: A<*>B ==> \
@@ -286,7 +286,7 @@
qed "qsum_subset_iff";
goal thy "A <+> B = C <+> D <-> A=C & B=D";
-by (simp_tac (!simpset addsimps [extension,qsum_subset_iff]) 1);
+by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1);
by (Blast_tac 1);
qed "qsum_equal_iff";
@@ -309,7 +309,7 @@
\ |] ==> qcase(c,d,u) : C(u)";
by (rtac (major RS qsumE) 1);
by (ALLGOALS (etac ssubst));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "qcase_type";
(** Rules for the Part primitive **)