src/HOL/Tools/inductive_realizer.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18929 d81435108688
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 21 23:02:14 2006 +0100
@@ -467,7 +467,7 @@
     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   end
 
-fun rlz_attrib arg (thy, thm) =
+fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
   let
     fun err () = error "ind_realizer: bad rule";
     val sets =
@@ -476,21 +476,19 @@
          | xs => map (set_of o fst o HOLogic.dest_imp) xs)
          handle TERM _ => err () | Empty => err ();
   in 
-    (add_ind_realizers (hd sets) (case arg of
+    add_ind_realizers (hd sets)
+      (case arg of
         NONE => sets | SOME NONE => []
       | SOME (SOME sets') => sets \\ sets')
-      thy, thm)
-  end;
+  end);
 
-val rlz_attrib_global = Attrib.syntax
+val ind_realizer = Attrib.syntax
  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     Scan.option (Scan.lift (Args.colon) |--
-      Scan.repeat1 Args.global_const))) >> rlz_attrib);
+      Scan.repeat1 Args.const))) >> rlz_attrib);
 
 val setup =
-  Attrib.add_attributes [("ind_realizer",
-    (rlz_attrib_global, K Attrib.undef_local_attribute),
-    "add realizers for inductive set")];
+  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
 
 end;