src/Pure/type.ML
changeset 20548 8ef25fe585a8
parent 20071 8f3e1ddb50e6
child 20674 93baed0f741c
     1.1 --- a/src/Pure/type.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4        (case AList.lookup (op =) fmap f of
     1.5          NONE => TFree f
     1.6        | SOME xi => TVar (xi, S));
     1.7 -  in (map_term_types (map_type_tfree thaw) t, fmap) end;
     1.8 +  in (map_types (map_type_tfree thaw) t, fmap) end;
     1.9  
    1.10  
    1.11  (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
    1.12 @@ -277,8 +277,8 @@
    1.13    in
    1.14      (case alist of
    1.15        [] => (t, fn x => x) (*nothing to do!*)
    1.16 -    | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
    1.17 -      map_term_types (map_type_tfree (thaw_one (map swap alist)))))
    1.18 +    | _ => (map_types (map_type_tvar (freeze_one alist)) t,
    1.19 +      map_types (map_type_tfree (thaw_one (map swap alist)))))
    1.20    end;
    1.21  
    1.22  val freeze = #1 o freeze_thaw;