src/HOL/Tools/Datatype/datatype_data.ML

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -436,7 +436,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+    |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;