diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Mar 27 14:19:18 2013 +0100
@@ -86,7 +86,7 @@
         (HOL_basic_ss addsimps
           (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)));
     fun prove prop =
-      Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+      Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
   in (map prove (triv_injects @ injects @ distincts), prove refl) end;