replaced setsolver ... by addsolver
authoroheimb
Fri, 12 Jul 1996 16:52:29 +0200
changeset 1853 c18ccd5631e0
parent 1852 289ce6cb5c84
child 1854 563dd2b25e37
replaced setsolver ... by addsolver
src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Thu Jul 11 15:30:22 1996 +0200
+++ b/src/HOLCF/Cfun3.ML	Fri Jul 12 16:52:29 1996 +0200
@@ -391,7 +391,4 @@
 (* use cont_tac as autotac.                                                *)
 (* ------------------------------------------------------------------------ *)
 
-simpset := !simpset setsolver 
-           (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
-                       (fn i => DEPTH_SOLVE_1 (cont_tac i))
-           );
+simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac i));