src/HOL/Tools/inductive_realizer.ML
changeset 30528 7173bf123335
parent 30435 e62d6ecab6ad
child 30722 623d4831c8cf
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -505,13 +505,13 @@
     1.4        | SOME (SOME sets') => sets \\ sets')
     1.5    end I);
     1.6  
     1.7 -val ind_realizer = Attrib.syntax
     1.8 - ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     1.9 +val ind_realizer =
    1.10 +  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    1.11      Scan.option (Scan.lift (Args.colon) |--
    1.12 -      Scan.repeat1 Args.const))) >> rlz_attrib);
    1.13 +      Scan.repeat1 Args.const))) >> rlz_attrib;
    1.14  
    1.15  val setup =
    1.16 -  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
    1.17 +  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
    1.18  
    1.19  end;
    1.20