src/HOL/Tools/recdef_package.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30528 7173bf123335
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4      val _ = requires_recdef thy;
     1.5  
     1.6      val name = Sign.intern_const thy raw_name;
     1.7 -    val bname = NameSpace.base_name name;
     1.8 +    val bname = Long_Name.base_name name;
     1.9      val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
    1.10  
    1.11      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.12 @@ -233,7 +233,7 @@
    1.13  fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
    1.14    let
    1.15      val name = Sign.intern_const thy raw_name;
    1.16 -    val bname = NameSpace.base_name name;
    1.17 +    val bname = Long_Name.base_name name;
    1.18  
    1.19      val _ = requires_recdef thy;
    1.20      val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");