adm_tac/cont_tacRs: proper simpset;

--- a/src/HOLCF/HOLCF.thy	Fri Sep 23 22:21:51 2005 +0200
+++ b/src/HOLCF/HOLCF.thy	Fri Sep 23 22:21:52 2005 +0200
@@ -22,7 +22,8 @@
 
 ML_setup {*
   simpset_ref() := simpset() addSolver
-     (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
+    (mk_solver' "adm_tac" (fn ss =>
+      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)));
 *}
 
 end

--- 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;
 *}