# HG changeset patch
# User wenzelm
# Date 1127506912 -7200
# Node ID 5b37787d2d9ef36584dcb960f52cc72953285c53
# Parent  61556de6ef4656ca43dee7ca4bf7b288f44b22d8
adm_tac/cont_tacRs: proper simpset;

diff -r 61556de6ef46 -r 5b37787d2d9e 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
diff -r 61556de6ef46 -r 5b37787d2d9e 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;
 *}