src/HOL/Tools/inductive_realizer.ML
changeset 20897 3f8d2834b2c4
parent 20071 8f3e1ddb50e6
child 20951 868120282837
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -467,7 +467,7 @@
     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   end
 
-fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
+fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
   let
     fun err () = error "ind_realizer: bad rule";
     val sets =
@@ -480,7 +480,7 @@
       (case arg of
         NONE => sets | SOME NONE => []
       | SOME (SOME sets') => sets \\ sets')
-  end);
+  end I);
 
 val ind_realizer = Attrib.syntax
  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--