src/HOL/Tools/typedef.ML

     fun contract_def NONE th = th
       | contract_def (SOME def_eq) th =
           let
             val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
             val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
-          in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
+          in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
       ObjectLogic.typedecl (t, vs, mx)
       #> snd
       #> Sign.add_consts_i

         ##>> pair set_def)
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
       #-> (fn ([type_definition], set_def) => fn thy1 =>
         let
-          fun make th = Drule.standard (th OF [type_definition]);
+          fun make th = Drule.export_without_context (th OF [type_definition]);
           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
             thy1
             |> Sign.add_path (Binding.name_of name)
             |> PureThy.add_thms