src/HOL/Tools/datatype_rep_proofs.ML
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -236,7 +236,7 @@
     1.4          val lhs = list_comb (Const (cname, constrT), l_args);
     1.5          val rhs = mk_univ_inj r_args n i;
     1.6          val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
     1.7 -        val def_name = NameSpace.base_name cname ^ "_def";
     1.8 +        val def_name = Long_Name.base_name cname ^ "_def";
     1.9          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.10            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    1.11          val ([def_thm], thy') =
    1.12 @@ -343,7 +343,7 @@
    1.13          
    1.14          val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
    1.15          val fTs = map fastype_of fs;
    1.16 -        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"),
    1.17 +        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
    1.18            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
    1.19              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
    1.20          val (def_thms, thy') =