tuned;
authorwenzelm
Mon Mar 10 17:52:30 2014 +0100 (2014-03-10)
changeset 560312e3329b89383
parent 56030 ef2ffd622264
child 56032 b034b9f0fa2a
tuned;
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Mon Mar 10 17:09:40 2014 +0100
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon Mar 10 17:52:30 2014 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4    let
     1.5      val ctxt = Proof_Context.init_global thy;
     1.6      val facts = args |> map (fn ((name, srcs), props) =>
     1.7 -      ((name, map (Attrib.attribute_cmd_global thy) srcs),
     1.8 +      ((name, map (Attrib.attribute_cmd ctxt) srcs),
     1.9          map (Thm.no_attributes o single o smart_cases ctxt) props));
    1.10    in thy |> Global_Theory.note_thmss "" facts |> snd end;
    1.11  
     2.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Mar 10 17:09:40 2014 +0100
     2.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Mar 10 17:52:30 2014 +0100
     2.3 @@ -560,7 +560,7 @@
     2.4      val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
     2.5        #> Syntax.check_terms ctxt;
     2.6  
     2.7 -    val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs;
     2.8 +    val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
     2.9      val sintrs = map fst intr_srcs ~~ intr_atts;
    2.10      val rec_tms = read_terms srec_tms;
    2.11      val dom_sum = singleton read_terms sdom_sum;