src/HOLCF/Lift.thy

--- a/src/HOLCF/Lift.thy	Fri Sep 23 22:21:51 2005 +0200
+++ b/src/HOLCF/Lift.thy	Fri Sep 23 22:21:52 2005 +0200
@@ -188,8 +188,8 @@
 fun cont_tacR i = REPEAT (cont_tac i);
 
 local val flift1_def = thm "flift1_def"
-in fun cont_tacRs i =
-  simp_tac (simpset()) i THEN
+in fun cont_tacRs ss i =
+  simp_tac ss i THEN
   REPEAT (cont_tac i)
 end;
 *}