--- a/src/Pure/term.ML Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/term.ML Thu Mar 05 12:08:00 2009 +0100
@@ -490,7 +490,7 @@
fun declare_term_names tm =
fold_aterms
- (fn Const (a, _) => Name.declare (NameSpace.base a)
+ (fn Const (a, _) => Name.declare (NameSpace.base_name a)
| Free (a, _) => Name.declare a
| _ => I) tm #>
fold_types declare_typ_names tm;
@@ -721,7 +721,7 @@
fun lambda v t =
let val x =
(case v of
- Const (x, _) => NameSpace.base x
+ Const (x, _) => NameSpace.base_name x
| Free (x, _) => x
| Var ((x, _), _) => x
| _ => Name.uu)