src/HOL/Tools/inductive_realizer.ML
changeset 18708 4b3dadb4fe33
parent 18358 0a733e11021a
child 18728 6790126ab5f6
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
 signature INDUCTIVE_REALIZER =
 sig
   val add_ind_realizers: string -> string list -> theory -> theory
-  val setup: (theory -> theory) list
+  val setup: theory -> theory
 end;
 
 structure InductiveRealizer : INDUCTIVE_REALIZER =
@@ -487,9 +487,10 @@
     Scan.option (Scan.lift (Args.colon) |--
       Scan.repeat1 Args.global_const))) >> rlz_attrib);
 
-val setup = [Attrib.add_attributes [("ind_realizer",
-  (rlz_attrib_global, K Attrib.undef_local_attribute),
-  "add realizers for inductive set")]];
+val setup =
+  Attrib.add_attributes [("ind_realizer",
+    (rlz_attrib_global, K Attrib.undef_local_attribute),
+    "add realizers for inductive set")];
 
 end;