src/Pure/term.ML
changeset 30364 577edc39b501
parent 30285 a135bfab6e83
child 32020 9abf5d66606e
     1.1 --- a/src/Pure/term.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/term.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -490,7 +490,7 @@
     1.4  
     1.5  fun declare_term_names tm =
     1.6    fold_aterms
     1.7 -    (fn Const (a, _) => Name.declare (NameSpace.base_name a)
     1.8 +    (fn Const (a, _) => Name.declare (Long_Name.base_name a)
     1.9        | Free (a, _) => Name.declare a
    1.10        | _ => I) tm #>
    1.11    fold_types declare_typ_names tm;
    1.12 @@ -721,7 +721,7 @@
    1.13  fun lambda v t =
    1.14    let val x =
    1.15      (case v of
    1.16 -      Const (x, _) => NameSpace.base_name x
    1.17 +      Const (x, _) => Long_Name.base_name x
    1.18      | Free (x, _) => x
    1.19      | Var ((x, _), _) => x
    1.20      | _ => Name.uu)