src/HOLCF/Tools/fixrec_package.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30485 99def5248e7f
     1.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4      val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
     1.5      
     1.6      fun one_def (l as Free(n,_)) r =
     1.7 -          let val b = NameSpace.base_name n
     1.8 +          let val b = Long_Name.base_name n
     1.9            in ((Binding.name (b^"_def"), []), r) end
    1.10        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
    1.11      fun defs [] _ = []
    1.12 @@ -230,7 +230,7 @@
    1.13  
    1.14  fun taken_names (t : term) : bstring list =
    1.15    let
    1.16 -    fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
    1.17 +    fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
    1.18        | taken (Free(a,_) , bs) = insert (op =) a bs
    1.19        | taken (f $ u     , bs) = taken (f, taken (u, bs))
    1.20        | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)