src/HOL/Tools/datatype_rep_proofs.ML
changeset 12922 ed70a600f0ea
parent 12180 91c9f661b183
child 13340 9b0332344ae2
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:05 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:34 2002 +0100
     1.3 @@ -44,7 +44,9 @@
     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 = theory "Datatype";
     1.8 +    val Datatype_thy =
     1.9 +      if PureThy.get_name thy = "Datatype" then thy
    1.10 +      else theory "Datatype";
    1.11      val node_name = "Datatype_Universe.node";
    1.12      val In0_name = "Datatype_Universe.In0";
    1.13      val In1_name = "Datatype_Universe.In1";