--- a/src/HOL/MiniML/Maybe.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/MiniML/Maybe.ML Mon Nov 03 12:13:18 1997 +0100
@@ -23,12 +23,12 @@
goal thy
"((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
-by(simp_tac (!simpset addsplits [split_option_bind]) 1);
+by(simp_tac (simpset() addsplits [split_option_bind]) 1);
qed "option_bind_eq_None";
Addsimps [option_bind_eq_None];
(* auxiliary lemma *)
goal Maybe.thy "(y = Some x) = (Some x = y)";
-by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
qed "rotate_Some";