src/HOL/Tools/inductive_realizer.ML
changeset 30722 623d4831c8cf
parent 30528 7173bf123335
child 31174 f1f1e9b53c81
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -505,13 +505,11 @@
     1.4        | SOME (SOME sets') => sets \\ sets')
     1.5    end I);
     1.6  
     1.7 -val ind_realizer =
     1.8 -  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     1.9 -    Scan.option (Scan.lift (Args.colon) |--
    1.10 -      Scan.repeat1 Args.const))) >> rlz_attrib;
    1.11 -
    1.12  val setup =
    1.13 -  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
    1.14 +  Attrib.setup @{binding ind_realizer}
    1.15 +    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    1.16 +      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
    1.17 +    "add realizers for inductive set";
    1.18  
    1.19  end;
    1.20