src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
           (expand_tuples_elim pre_elim))*)
         val elim =
-          (Drule.standard o Skip_Proof.make_thm thy)
+          (Drule.export_without_context o Skip_Proof.make_thm thy)
           (mk_casesrule (ProofContext.init thy) pred intros)
       in
         mk_pred_data ((intros, SOME elim), no_compilation)
       end
   | NONE => error ("No such predicate: " ^ quote name)

         "expected rules for " ^ constname ^ ", but received rules for " ^
           commas (map constname_of_intro pre_intros))
       else ()
     val pred = Const (constname, T)
     val pre_elim = 
-      (Drule.standard o Skip_Proof.make_thm thy)
+      (Drule.export_without_context o Skip_Proof.make_thm thy)
       (mk_casesrule (ProofContext.init thy) pred pre_intros)
   in register_predicate (constname, pre_intros, pre_elim) thy end
 
 fun defined_function_of compilation pred =
   let

 fun prove options thy clauses preds modes moded_clauses compiled_terms =
   map_preds_modes (prove_pred options thy clauses preds modes)
     (join_preds_modes moded_clauses compiled_terms)
 
 fun prove_by_skip options thy _ _ _ _ compiled_terms =
-  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
+  map_preds_modes
+    (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
     compiled_terms
 
 (* preparation of introduction rules into special datastructures *)
 
 fun dest_prem thy params t =

       let
         val intros = intros_of thy predname
         val elim = the_elim_of thy predname
         val nparams = nparams_of thy predname
         val elim' =
-          (Drule.standard o (Skip_Proof.make_thm thy))
+          (Drule.export_without_context o Skip_Proof.make_thm thy)
           (mk_casesrule (ProofContext.init thy) nparams intros)
       in
         if not (Thm.equiv_thm (elim, elim')) then
           error "Introduction and elimination rules do not match!"
         else true