src/HOL/Tools/inductive_realizer.ML

--- a/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -510,7 +510,7 @@
 val setup =
   Attrib.setup @{binding ind_realizer}
     ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
-      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
+      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
     "add realizers for inductive set";
 
 end;