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;