# HG changeset patch
# User oheimb
# Date 837183149 -7200
# Node ID c18ccd5631e07f4ee1f9e91e0e6fac9a996d6c27
# Parent  289ce6cb5c84a2b1d3abf7a81f475a99ea0942fa
replaced setsolver ... by addsolver

diff -r 289ce6cb5c84 -r c18ccd5631e0 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));