--- a/src/HOL/Tools/refute_isar.ML Mon Jan 28 22:27:19 2008 +0100
+++ b/src/HOL/Tools/refute_isar.ML Mon Jan 28 22:27:20 2008 +0100
@@ -19,13 +19,10 @@
(* the form [name1=value1, name2=value2, ...] *)
(* ------------------------------------------------------------------------- *)
- fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan)
- >> op :: || Scan.succeed [];
-
val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
val scan_parms = Scan.option
- (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
+ (OuterParse.$$$ "[" |-- (OuterParse.list scan_parm) --| OuterParse.$$$ "]");
(* ------------------------------------------------------------------------- *)
(* set up the 'refute' command *)