--- a/src/Provers/clasimp.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/clasimp.ML Sun Feb 13 17:15:14 2005 +0100
@@ -331,8 +331,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_PROP o auto_tac)
- | auto_meth (Some (m, n)) = clasimp_meth (CHANGED_PROP 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 *)