--- 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";