# HG changeset patch
# User wenzelm
# Date 1394470350 -3600
# Node ID 2e3329b89383b02046a7d3386b4e0f00484791b4
# Parent  ef2ffd622264700991c80966f539b82fa43ad2c2
tuned;

diff -r ef2ffd622264 -r 2e3329b89383 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon Mar 10 17:09:40 2014 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Mon Mar 10 17:52:30 2014 +0100
@@ -48,7 +48,7 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val facts = args |> map (fn ((name, srcs), props) =>
-      ((name, map (Attrib.attribute_cmd_global thy) srcs),
+      ((name, map (Attrib.attribute_cmd ctxt) srcs),
         map (Thm.no_attributes o single o smart_cases ctxt) props));
   in thy |> Global_Theory.note_thmss "" facts |> snd end;
 
diff -r ef2ffd622264 -r 2e3329b89383 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon Mar 10 17:09:40 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Mar 10 17:52:30 2014 +0100
@@ -560,7 +560,7 @@
     val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
       #> Syntax.check_terms ctxt;
 
-    val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs;
+    val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
     val sintrs = map fst intr_srcs ~~ intr_atts;
     val rec_tms = read_terms srec_tms;
     val dom_sum = singleton read_terms sdom_sum;