src/HOL/Tools/datatype_rep_proofs.ML
changeset 19540 d036bff01c23
parent 19346 c4c003abd830
child 20046 9c8909fc5865
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue May 02 20:42:35 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue May 02 20:42:36 2006 +0200
     1.3 @@ -42,9 +42,7 @@
     1.4  fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
     1.5        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
     1.6    let
     1.7 -    val Datatype_thy =
     1.8 -      if Context.theory_name thy = "Datatype" then thy
     1.9 -      else theory "Datatype";
    1.10 +    val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    1.11      val node_name = "Datatype_Universe.node";
    1.12      val In0_name = "Datatype_Universe.In0";
    1.13      val In1_name = "Datatype_Universe.In1";