--- 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;