Context.theory_name;

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jun 17 18:33:15 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jun 17 18:33:16 2005 +0200
@@ -43,7 +43,7 @@
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val Datatype_thy =
-      if PureThy.get_name thy = "Datatype" then thy
+      if Context.theory_name thy = "Datatype" then thy
       else theory "Datatype";
     val node_name = "Datatype_Universe.node";
     val In0_name = "Datatype_Universe.In0";