src/HOL/Tools/choice_specification.ML

 end
 
 fun add_specification axiomatic cos arg =
     arg |> apsnd Thm.freezeT
         |> proc_exprop axiomatic cos
-        |> apsnd Drule.standard
+        |> apsnd Drule.export_without_context
 
 
 (* Collect all intances of constants in term *)
 
 fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))

                             else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
                                   PureThy.store_thm (Binding.name name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
-                             |> apsnd Drule.standard
+                             |> apsnd Drule.export_without_context
                              |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
                              |> add_final
                              |> Library.swap
                     end