src/HOL/Tools/datatype_rep_proofs.ML
changeset 16431 90c9b8bb3b66
parent 16287 7a03b4b4df67
child 16486 1a12cdb6ee6b
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jun 17 18:33:15 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jun 17 18:33:16 2005 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
     1.5    let
     1.6      val Datatype_thy =
     1.7 -      if PureThy.get_name thy = "Datatype" then thy
     1.8 +      if Context.theory_name thy = "Datatype" then thy
     1.9        else theory "Datatype";
    1.10      val node_name = "Datatype_Universe.node";
    1.11      val In0_name = "Datatype_Universe.In0";