varify returns newly introduced variables;
authorwenzelm
Fri Dec 14 11:54:47 2001 +0100 (2001-12-14 ago)
changeset 1250136b2ac65e18d
parent 12500 0a6667d65e9b
child 12502 9e7f72e25022
varify returns newly introduced variables;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Fri Dec 14 11:54:13 2001 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Dec 14 11:54:47 2001 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val no_tvars: typ -> typ
     1.5    val varifyT: typ -> typ
     1.6    val unvarifyT: typ -> typ
     1.7 -  val varify: term * string list -> term
     1.8 +  val varify: term * string list -> term * (string * indexname) list
     1.9    val freeze_thaw_type : typ -> typ * (typ -> typ)
    1.10    val freeze_thaw : term -> term * (term -> term)
    1.11  
    1.12 @@ -84,8 +84,9 @@
    1.13  (*** TFrees and TVars ***)
    1.14  
    1.15  fun no_tvars T =
    1.16 -  if null (typ_tvars T) then T
    1.17 -  else raise TYPE ("Illegal schematic type variable(s)", [T], []);
    1.18 +  (case typ_tvars T of [] => T
    1.19 +  | vs => raise TYPE ("Illegal schematic type variable(s): " ^
    1.20 +      commas (map (Syntax.string_of_vname o #1) vs), [T], []));
    1.21  
    1.22  
    1.23  (* varify, unvarify *)
    1.24 @@ -100,12 +101,12 @@
    1.25    let
    1.26      val fs = add_term_tfree_names (t, []) \\ fixed;
    1.27      val ixns = add_term_tvar_ixns (t, []);
    1.28 -    val fmap = fs ~~ variantlist (fs, map #1 ixns)
    1.29 +    val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
    1.30      fun thaw (f as (a, S)) =
    1.31        (case assoc (fmap, a) of
    1.32          None => TFree f
    1.33 -      | Some b => TVar ((b, 0), S));
    1.34 -  in map_term_types (map_type_tfree thaw) t end;
    1.35 +      | Some b => TVar (b, S));
    1.36 +  in (map_term_types (map_type_tfree thaw) t, fmap) end;
    1.37  
    1.38  
    1.39  (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)