src/Provers/clasimp.ML
changeset 36960 01594f816e3a
parent 36601 8a041e2d8122
child 37720 50a9e2fa4f6b
--- a/src/Provers/clasimp.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/clasimp.ML	Mon May 17 23:54:15 2010 +0200
@@ -275,7 +275,7 @@
   Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
 
 val auto_method =
-  Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
     Method.sections clasimp_modifiers >>
   (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
     | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));