src/ZF/Tools/ind_cases.ML
changeset 47815 43f677b3ae91
parent 46961 5c6955f487e5
child 54742 7a86358a3c0b
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Apr 27 22:47:30 2012 +0200
     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 thy) srcs),
     1.8 +      ((name, map (Attrib.attribute_cmd_global thy) 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