src/ZF/Tools/inductive_package.ML
changeset 47815 43f677b3ae91
parent 46961 5c6955f487e5
child 50239 fb579401dc26
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -558,7 +558,7 @@
     1.4      val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
     1.5        #> Syntax.check_terms ctxt;
     1.6  
     1.7 -    val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
     1.8 +    val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs;
     1.9      val sintrs = map fst intr_srcs ~~ intr_atts;
    1.10      val rec_tms = read_terms srec_tms;
    1.11      val dom_sum = singleton read_terms sdom_sum;