# HG changeset patch
# User wenzelm
# Date 1119025996 -7200
# Node ID 90c9b8bb3b66563c1a0b1dd67775f5548ddc2036
# Parent  bc07926e4f0357b02e2fce991ca305150c54ed8a
Context.theory_name;

diff -r bc07926e4f03 -r 90c9b8bb3b66 src/HOL/Tools/datatype_rep_proofs.ML
--- 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";