--- a/src/Provers/clasimp.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/clasimp.ML Sun Jan 07 21:41:56 2001 +0100
@@ -315,8 +315,8 @@
fun auto_args m =
Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
-fun auto_meth None = clasimp_meth (CHANGED o auto_tac)
- | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n));
+fun auto_meth None = clasimp_meth (CHANGED_PROP o auto_tac)
+ | auto_meth (Some (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
(* theory setup *)
@@ -330,6 +330,6 @@
("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
("force", clasimp_method' force_tac, "force"),
("auto", auto_args auto_meth, "auto"),
- ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
+ ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]];
end;