src/HOL/Tools/inductive_realizer.ML
changeset 18708 4b3dadb4fe33
parent 18358 0a733e11021a
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  signature INDUCTIVE_REALIZER =
     1.5  sig
     1.6    val add_ind_realizers: string -> string list -> theory -> theory
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure InductiveRealizer : INDUCTIVE_REALIZER =
    1.12 @@ -487,9 +487,10 @@
    1.13      Scan.option (Scan.lift (Args.colon) |--
    1.14        Scan.repeat1 Args.global_const))) >> rlz_attrib);
    1.15  
    1.16 -val setup = [Attrib.add_attributes [("ind_realizer",
    1.17 -  (rlz_attrib_global, K Attrib.undef_local_attribute),
    1.18 -  "add realizers for inductive set")]];
    1.19 +val setup =
    1.20 +  Attrib.add_attributes [("ind_realizer",
    1.21 +    (rlz_attrib_global, K Attrib.undef_local_attribute),
    1.22 +    "add realizers for inductive set")];
    1.23  
    1.24  end;
    1.25