# HG changeset patch
# User wenzelm
# Date 1201555640 -3600
# Node ID b629b4f2026ca09bd8ff076bb4ec20be55a65e31
# Parent  f8bcd311d50136554556eac1eb1bfcc3adc57f3f
removed redundant repeatd scanner combinator;

diff -r f8bcd311d501 -r b629b4f2026c src/HOL/Tools/refute_isar.ML
--- 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                                               *)