src/HOLCF/HOLCF.thy

--- 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