--- a/src/HOL/IMP/Expr.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/IMP/Expr.ML Mon Nov 03 12:13:18 1997 +0100
@@ -35,12 +35,12 @@
goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)";
by (aexp.induct_tac "a" 1); (* struct. ind. *)
by (ALLGOALS Simp_tac); (* rewr. Den. *)
-by (TRYALL (fast_tac (!claset addSIs (evala.intrs@prems)
+by (TRYALL (fast_tac (claset() addSIs (evala.intrs@prems)
addSEs evala_elim_cases)));
qed_spec_mp "aexp_iff";
goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)";
by (bexp.induct_tac "b" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
+by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong]
addsimps (aexp_iff::evalb_simps))));
qed_spec_mp "bexp_iff";