src/Provers/clasimp.ML

 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
 
 
 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));