--- a/src/HOL/Tools/inductive_realizer.ML Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Sep 18 16:47:40 2014 +0200
@@ -8,7 +8,6 @@
signature INDUCTIVE_REALIZER =
sig
val add_ind_realizers: string -> string list -> theory -> theory
- val setup: theory -> theory
end;
structure InductiveRealizer : INDUCTIVE_REALIZER =
@@ -513,11 +512,10 @@
| SOME (SOME sets') => subtract (op =) sets' sets)
end I);
-val setup =
- Attrib.setup @{binding ind_realizer}
- ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
- Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
- "add realizers for inductive set";
+val _ = Theory.setup (Attrib.setup @{binding ind_realizer}
+ ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+ Scan.option (Scan.lift (Args.colon) |--
+ Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
+ "add realizers for inductive set");
end;