--- a/src/HOL/Tools/recdef_package.ML Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Sun Mar 08 17:26:14 2009 +0100
@@ -193,7 +193,7 @@
val _ = requires_recdef thy;
val name = Sign.intern_const thy raw_name;
- val bname = NameSpace.base_name name;
+ val bname = Long_Name.base_name name;
val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
@@ -233,7 +233,7 @@
fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
let
val name = Sign.intern_const thy raw_name;
- val bname = NameSpace.base_name name;
+ val bname = Long_Name.base_name name;
val _ = requires_recdef thy;
val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");