--- a/src/HOLCF/Up2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Up2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -26,7 +26,7 @@
qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1a]) 1)
+ (simp_tac (simpset() addsimps [less_up1a]) 1)
]);
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
@@ -45,13 +45,13 @@
qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1b]) 1)
+ (simp_tac (simpset() addsimps [less_up1b]) 1)
]);
qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1c]) 1)
+ (simp_tac (simpset() addsimps [less_up1c]) 1)
]);
(* ------------------------------------------------------------------------ *)