# HG changeset patch
# User wenzelm
# Date 1146595356 -7200
# Node ID d036bff01c2347ae5205c2f059abbd5d4c70f33c
# Parent  5b37bb0ad96483bea3efa185253a1ead6ff0acd0
ThyInfo.the_theory;

diff -r 5b37bb0ad964 -r d036bff01c23 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue May 02 20:42:35 2006 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue May 02 20:42:36 2006 +0200
@@ -42,9 +42,7 @@
 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
-    val Datatype_thy =
-      if Context.theory_name thy = "Datatype" then thy
-      else theory "Datatype";
+    val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
     val node_name = "Datatype_Universe.node";
     val In0_name = "Datatype_Universe.In0";
     val In1_name = "Datatype_Universe.In1";