src/HOL/Tools/inductive_realizer.ML
changeset 55954 a29aefc88c8d
parent 55235 4b4627f5912b
child 55958 4ec984df4f45
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 13:44:01 2014 +0100
     1.3 @@ -515,7 +515,8 @@
     1.4  val setup =
     1.5    Attrib.setup @{binding ind_realizer}
     1.6      ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     1.7 -      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
     1.8 +      Scan.option (Scan.lift (Args.colon) |--
     1.9 +        Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
    1.10      "add realizers for inductive set";
    1.11  
    1.12  end;