--- a/src/HOL/Tools/datatype_realizer.ML Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Sun Mar 08 17:26:14 2009 +0100
@@ -168,7 +168,7 @@
val Ts = map (typ_of_dtyp descr sorts) cargs;
val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
- val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
+ val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
(HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $