src/HOL/Tools/typedef_package.ML

        ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
       |> add_def (Logic.mk_defpair (setC, set))
       ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
-          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
+          [apsnd (fn cond_axm => nonempty RS cond_axm)])]
       ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps
       |-> (fn (set_def, [type_definition]) => fn thy1 =>
         let
           fun make th = Drule.standard (th OF [type_definition]);

   let
     val name = the_default (#1 typ) opt_name;
     val (cset, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
-    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
+    val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   in
     Context.Theory thy
     |> typedef_result non_empty
     ||> Context.the_theory