export freeze_thaw_type;
authorwenzelm
Sat Nov 18 19:48:34 2000 +0100 (2000-11-18 ago)
changeset 10495284ee538991c
parent 10494 305b37c8d8a3
child 10496 f2d304bdf3cc
export freeze_thaw_type;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Sat Nov 18 19:48:07 2000 +0100
     1.2 +++ b/src/Pure/type.ML	Sat Nov 18 19:48:34 2000 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    val varifyT: typ -> typ
     1.5    val unvarifyT: typ -> typ
     1.6    val varify: term * string list -> term
     1.7 +  val freeze_thaw_type : typ -> typ * (typ -> typ)
     1.8    val freeze_thaw : term -> term * (term -> term)
     1.9  
    1.10    (*type signatures*)
    1.11 @@ -123,7 +124,9 @@
    1.12  fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
    1.13        handle OPTION => TFree(a,sort);
    1.14  
    1.15 -(*this sort of code could replace unvarifyT (?) -- currently unused*)
    1.16 +in
    1.17 +
    1.18 +(*this sort of code could replace unvarifyT*)
    1.19  fun freeze_thaw_type T =
    1.20    let
    1.21      val used = add_typ_tfree_names (T, [])
    1.22 @@ -131,8 +134,6 @@
    1.23      val (alist, _) = foldr new_name (tvars, ([], used));
    1.24    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
    1.25  
    1.26 -in
    1.27 -
    1.28  fun freeze_thaw t =
    1.29    let
    1.30      val used = it_term_types add_typ_tfree_names (t, [])