--- a/src/HOL/Decision_Procs/Approximation.thy Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon May 17 23:54:15 2010 +0200
@@ -3310,13 +3310,13 @@
by auto
method_setup approximation = {*
- Scan.lift (OuterParse.nat)
+ Scan.lift Parse.nat
--
Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
- |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+ |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
--
Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
- |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
+ |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
>>
(fn ((prec, splitting), taylor) => fn ctxt =>
SIMPLE_METHOD' (fn i =>