Context.theory_name;
authorwenzelm
Fri Jun 17 18:33:16 2005 +0200 (2005-06-17)
changeset 1643190c9b8bb3b66
parent 16430 bc07926e4f03
child 16432 a6e8fb94a8ca
Context.theory_name;
src/HOL/Tools/datatype_rep_proofs.ML
     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";