diff -r 4dd3d5efcc7f -r a1e409db516b src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/clasimp.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -302,7 +302,8 @@
 
 
 fun auto_args m =
-  Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
+  Method.bang_sectioned_args' clasimp_modifiers
+    (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.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));