--- a/src/HOL/Tools/inductive_realizer.ML Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 06 13:44:01 2014 +0100
@@ -515,7 +515,8 @@
val setup =
Attrib.setup @{binding ind_realizer}
((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
- Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
+ Scan.option (Scan.lift (Args.colon) |--
+ Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
"add realizers for inductive set";
end;