simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
authorwenzelm
Mon Sep 13 11:35:55 2010 +0200 (2010-09-13)
changeset 3929427fae73fe769
parent 39293 651e5a3e8cfd
child 39295 6e8b0672c6a2
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Sep 13 00:10:29 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Sep 13 11:35:55 2010 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val anyT: sort -> typ
     1.6    val is_param: indexname -> bool
     1.7 +  val is_paramT: typ -> bool
     1.8    val param: int -> string * sort -> typ
     1.9    val paramify_vars: typ -> typ
    1.10    val paramify_dummies: typ -> int -> typ * int
    1.11 @@ -28,8 +29,14 @@
    1.12  (* type inference parameters -- may get instantiated *)
    1.13  
    1.14  fun is_param (x, _: int) = String.isPrefix "?" x;
    1.15 +
    1.16 +fun is_paramT (TVar (xi, _)) = is_param xi
    1.17 +  | is_paramT _ = false;
    1.18 +
    1.19  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.20  
    1.21 +fun mk_param i S = TVar (("?'a", i), S);
    1.22 +
    1.23  val paramify_vars =
    1.24    Same.commit
    1.25      (Term_Subst.map_atypsT_same
    1.26 @@ -62,76 +69,42 @@
    1.27  
    1.28  
    1.29  
    1.30 -(** pretyps and preterms **)
    1.31 -
    1.32 -datatype pretyp =
    1.33 -  PType of string * pretyp list |
    1.34 -  PTFree of string * sort |
    1.35 -  PTVar of indexname * sort |
    1.36 -  Param of int * sort;
    1.37 -
    1.38 -datatype preterm =
    1.39 -  PConst of string * pretyp |
    1.40 -  PFree of string * pretyp |
    1.41 -  PVar of indexname * pretyp |
    1.42 -  PBound of int |
    1.43 -  PAbs of string * pretyp * preterm |
    1.44 -  PAppl of preterm * preterm;
    1.45 -
    1.46 -
    1.47 -(* utils *)
    1.48 +(** prepare types/terms: create inference parameters **)
    1.49  
    1.50 -fun deref tye (T as Param (i, S)) =
    1.51 -      (case Inttab.lookup tye i of
    1.52 -        NONE => T
    1.53 -      | SOME U => deref tye U)
    1.54 -  | deref tye T = T;
    1.55 +(* prepare_typ *)
    1.56  
    1.57 -fun fold_pretyps f (PConst (_, T)) x = f T x
    1.58 -  | fold_pretyps f (PFree (_, T)) x = f T x
    1.59 -  | fold_pretyps f (PVar (_, T)) x = f T x
    1.60 -  | fold_pretyps _ (PBound _) x = x
    1.61 -  | fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
    1.62 -  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x);
    1.63 -
    1.64 -
    1.65 -
    1.66 -(** raw typs/terms to pretyps/preterms **)
    1.67 -
    1.68 -(* pretyp_of *)
    1.69 -
    1.70 -fun pretyp_of typ params_idx =
    1.71 +fun prepare_typ typ params_idx =
    1.72    let
    1.73      val (params', idx) = fold_atyps
    1.74        (fn TVar (xi as (x, _), S) =>
    1.75            (fn ps_idx as (ps, idx) =>
    1.76              if is_param xi andalso not (Vartab.defined ps xi)
    1.77 -            then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx)
    1.78 +            then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
    1.79          | _ => I) typ params_idx;
    1.80  
    1.81 -    fun pre_of (TVar (v as (xi, _))) idx =
    1.82 +    fun prepare (T as Type (a, Ts)) idx =
    1.83 +          if T = dummyT then (mk_param idx [], idx + 1)
    1.84 +          else
    1.85 +            let val (Ts', idx') = fold_map prepare Ts idx
    1.86 +            in (Type (a, Ts'), idx') end
    1.87 +      | prepare (T as TVar (xi, _)) idx =
    1.88            (case Vartab.lookup params' xi of
    1.89 -            NONE => PTVar v
    1.90 +            NONE => T
    1.91            | SOME p => p, idx)
    1.92 -      | pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1)
    1.93 -      | pre_of (TFree v) idx = (PTFree v, idx)
    1.94 -      | pre_of (T as Type (a, Ts)) idx =
    1.95 -          if T = dummyT then (Param (idx, []), idx + 1)
    1.96 -          else
    1.97 -            let val (Ts', idx') = fold_map pre_of Ts idx
    1.98 -            in (PType (a, Ts'), idx') end;
    1.99 +      | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
   1.100 +      | prepare (T as TFree _) idx = (T, idx);
   1.101  
   1.102 -    val (ptyp, idx') = pre_of typ idx;
   1.103 -  in (ptyp, (params', idx')) end;
   1.104 +    val (typ', idx') = prepare typ idx;
   1.105 +  in (typ', (params', idx')) end;
   1.106  
   1.107  
   1.108 -(* preterm_of *)
   1.109 +(* prepare_term *)
   1.110  
   1.111 -fun preterm_of const_type tm (vparams, params, idx) =
   1.112 +fun prepare_term const_type tm (vparams, params, idx) =
   1.113    let
   1.114      fun add_vparm xi (ps_idx as (ps, idx)) =
   1.115        if not (Vartab.defined ps xi) then
   1.116 -        (Vartab.update (xi, Param (idx, [])) ps, idx + 1)
   1.117 +        (Vartab.update (xi, mk_param idx []) ps, idx + 1)
   1.118        else ps_idx;
   1.119  
   1.120      val (vparams', idx') = fold_aterms
   1.121 @@ -142,109 +115,96 @@
   1.122        tm (vparams, idx);
   1.123      fun var_param xi = the (Vartab.lookup vparams' xi);
   1.124  
   1.125 -    fun polyT_of T idx = apsnd snd (pretyp_of (paramify_vars T) (Vartab.empty, idx));
   1.126 +    fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
   1.127  
   1.128      fun constraint T t ps =
   1.129        if T = dummyT then (t, ps)
   1.130        else
   1.131 -        let val (T', ps') = pretyp_of T ps
   1.132 -        in (PAppl (PConst ("_type_constraint_", PType ("fun", [T', T'])), t), ps') end;
   1.133 +        let val (T', ps') = prepare_typ T ps
   1.134 +        in (Type.constraint T' t, ps') end;
   1.135  
   1.136 -    fun pre_of (Const (c, T)) (ps, idx) =
   1.137 +    fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
   1.138 +          let
   1.139 +            val (T', ps_idx') = prepare_typ T ps_idx;
   1.140 +            val (t', ps_idx'') = prepare t ps_idx';
   1.141 +          in (Const ("_type_constraint_", T') $ t', ps_idx'') end
   1.142 +      | prepare (Const (c, T)) (ps, idx) =
   1.143            (case const_type c of
   1.144              SOME U =>
   1.145 -              let val (pU, idx') = polyT_of U idx
   1.146 -              in constraint T (PConst (c, pU)) (ps, idx') end
   1.147 +              let val (U', idx') = polyT_of U idx
   1.148 +              in constraint T (Const (c, U')) (ps, idx') end
   1.149            | NONE => error ("Undeclared constant: " ^ quote c))
   1.150 -      | pre_of (Const ("_type_constraint_", T) $ t) ps_idx =
   1.151 +      | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
   1.152 +          let val (T', idx') = polyT_of T idx
   1.153 +          in (Var (xi, T'), (ps, idx')) end
   1.154 +      | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
   1.155 +      | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
   1.156 +      | prepare (Bound i) ps_idx = (Bound i, ps_idx)
   1.157 +      | prepare (Abs (x, T, t)) ps_idx =
   1.158            let
   1.159 -            val (T', ps_idx') = pretyp_of T ps_idx;
   1.160 -            val (t', ps_idx'') = pre_of t ps_idx';
   1.161 -          in (PAppl (PConst ("_type_constraint_", T'), t'), ps_idx'') end
   1.162 -      | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
   1.163 -          let val (pT, idx') = polyT_of T idx
   1.164 -          in (PVar (xi, pT), (ps, idx')) end
   1.165 -      | pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx
   1.166 -      | pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx
   1.167 -      | pre_of (Bound i) ps_idx = (PBound i, ps_idx)
   1.168 -      | pre_of (Abs (x, T, t)) ps_idx =
   1.169 +            val (T', ps_idx') = prepare_typ T ps_idx;
   1.170 +            val (t', ps_idx'') = prepare t ps_idx';
   1.171 +          in (Abs (x, T', t'), ps_idx'') end
   1.172 +      | prepare (t $ u) ps_idx =
   1.173            let
   1.174 -            val (T', ps_idx') = pretyp_of T ps_idx;
   1.175 -            val (t', ps_idx'') = pre_of t ps_idx';
   1.176 -          in (PAbs (x, T', t'), ps_idx'') end
   1.177 -      | pre_of (t $ u) ps_idx =
   1.178 -          let
   1.179 -            val (t', ps_idx') = pre_of t ps_idx;
   1.180 -            val (u', ps_idx'') = pre_of u ps_idx';
   1.181 -          in (PAppl (t', u'), ps_idx'') end;
   1.182 +            val (t', ps_idx') = prepare t ps_idx;
   1.183 +            val (u', ps_idx'') = prepare u ps_idx';
   1.184 +          in (t' $ u', ps_idx'') end;
   1.185  
   1.186 -    val (tm', (params', idx'')) = pre_of tm (params, idx');
   1.187 +    val (tm', (params', idx'')) = prepare tm (params, idx');
   1.188    in (tm', (vparams', params', idx'')) end;
   1.189  
   1.190  
   1.191  
   1.192 -(** pretyps/terms to typs/terms **)
   1.193 +(** finish types/terms: standardize remaining parameters **)
   1.194  
   1.195 -(* add_parms *)
   1.196 +(* dereferenced views *)
   1.197  
   1.198 -fun add_parmsT tye T =
   1.199 +fun deref tye (T as TVar (xi, _)) =
   1.200 +      (case Vartab.lookup tye xi of
   1.201 +        NONE => T
   1.202 +      | SOME U => deref tye U)
   1.203 +  | deref tye T = T;
   1.204 +
   1.205 +fun add_parms tye T =
   1.206    (case deref tye T of
   1.207 -    PType (_, Ts) => fold (add_parmsT tye) Ts
   1.208 -  | Param (i, _) => insert (op =) i
   1.209 +    Type (_, Ts) => fold (add_parms tye) Ts
   1.210 +  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
   1.211    | _ => I);
   1.212  
   1.213 -fun add_parms tye = fold_pretyps (add_parmsT tye);
   1.214 -
   1.215 -
   1.216 -(* add_names *)
   1.217 -
   1.218 -fun add_namesT tye T =
   1.219 +fun add_names tye T =
   1.220    (case deref tye T of
   1.221 -    PType (_, Ts) => fold (add_namesT tye) Ts
   1.222 -  | PTFree (x, _) => Name.declare x
   1.223 -  | PTVar ((x, _), _) => Name.declare x
   1.224 -  | Param _ => I);
   1.225 -
   1.226 -fun add_names tye = fold_pretyps (add_namesT tye);
   1.227 +    Type (_, Ts) => fold (add_names tye) Ts
   1.228 +  | TFree (x, _) => Name.declare x
   1.229 +  | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
   1.230  
   1.231  
   1.232 -(* simple_typ/term_of *)
   1.233 -
   1.234 -fun simple_typ_of tye f T =
   1.235 -  (case deref tye T of
   1.236 -    PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts)
   1.237 -  | PTFree v => TFree v
   1.238 -  | PTVar v => TVar v
   1.239 -  | Param (i, S) => TVar (f i, S));
   1.240 +(* finish *)
   1.241  
   1.242 -fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
   1.243 -  | simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T)
   1.244 -  | simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T)
   1.245 -  | simple_term_of tye f (PBound i) = Bound i
   1.246 -  | simple_term_of tye f (PAbs (x, T, t)) =
   1.247 -      Abs (x, simple_typ_of tye f T, simple_term_of tye f t)
   1.248 -  | simple_term_of tye f (PAppl (t, u)) =
   1.249 -      simple_term_of tye f t $ simple_term_of tye f u;
   1.250 -
   1.251 +fun finish ctxt tye (Ts, ts) =
   1.252 +  let
   1.253 +    val used =
   1.254 +      (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
   1.255 +    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
   1.256 +    val names = Name.invents used ("?" ^ Name.aT) (length parms);
   1.257 +    val tab = Vartab.make (parms ~~ names);
   1.258 +    val idx = Variable.maxidx_of ctxt + 1;
   1.259  
   1.260 -(* typs_terms_of *)
   1.261 -
   1.262 -fun typs_terms_of ctxt tye (Ts, ts) =
   1.263 -  let
   1.264 -    val used = fold (add_names tye) ts (fold (add_namesT tye) Ts (Variable.names_of ctxt));
   1.265 -    val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts []));
   1.266 -    val names = Name.invents used ("?" ^ Name.aT) (length parms);
   1.267 -    val tab = Inttab.make (parms ~~ names);
   1.268 -
   1.269 -    val maxidx = Variable.maxidx_of ctxt;
   1.270 -    fun f i = (the (Inttab.lookup tab i), maxidx + 1);
   1.271 -  in (map (simple_typ_of tye f) Ts, map (Type.strip_constraints o simple_term_of tye f) ts) end;
   1.272 +    fun finish_typ T =
   1.273 +      (case deref tye T of
   1.274 +        Type (a, Ts) => Type (a, map finish_typ Ts)
   1.275 +      | U as TFree _ => U
   1.276 +      | U as TVar (xi, S) =>
   1.277 +          (case Vartab.lookup tab xi of
   1.278 +            NONE => U
   1.279 +          | SOME a => TVar ((a, idx), S)));
   1.280 +  in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
   1.281  
   1.282  
   1.283  
   1.284  (** order-sorted unification of types **)
   1.285  
   1.286 -exception NO_UNIFIER of string * pretyp Inttab.table;
   1.287 +exception NO_UNIFIER of string * typ Vartab.table;
   1.288  
   1.289  fun unify ctxt pp =
   1.290    let
   1.291 @@ -259,17 +219,15 @@
   1.292          Syntax.string_of_sort ctxt S;
   1.293  
   1.294      fun meet (_, []) tye_idx = tye_idx
   1.295 -      | meet (Param (i, S'), S) (tye_idx as (tye, idx)) =
   1.296 -          if Sign.subsort thy (S', S) then tye_idx
   1.297 -          else (Inttab.update_new (i,
   1.298 -            Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1)
   1.299 -      | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
   1.300 +      | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
   1.301            meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
   1.302 -      | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
   1.303 +      | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
   1.304            if Sign.subsort thy (S', S) then tye_idx
   1.305            else raise NO_UNIFIER (not_of_sort x S' S, tye)
   1.306 -      | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) =
   1.307 +      | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
   1.308            if Sign.subsort thy (S', S) then tye_idx
   1.309 +          else if is_param xi then
   1.310 +            (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
   1.311            else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
   1.312      and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
   1.313            meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
   1.314 @@ -278,20 +236,20 @@
   1.315  
   1.316      (* occurs check and assignment *)
   1.317  
   1.318 -    fun occurs_check tye i (Param (i', S)) =
   1.319 -          if i = i' then raise NO_UNIFIER ("Occurs check!", tye)
   1.320 +    fun occurs_check tye xi (TVar (xi', S)) =
   1.321 +          if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
   1.322            else
   1.323 -            (case Inttab.lookup tye i' of
   1.324 +            (case Vartab.lookup tye xi' of
   1.325                NONE => ()
   1.326 -            | SOME T => occurs_check tye i T)
   1.327 -      | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
   1.328 +            | SOME T => occurs_check tye xi T)
   1.329 +      | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
   1.330        | occurs_check _ _ _ = ();
   1.331  
   1.332 -    fun assign i (T as Param (i', _)) S tye_idx =
   1.333 -          if i = i' then tye_idx
   1.334 -          else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
   1.335 -      | assign i T S (tye_idx as (tye, _)) =
   1.336 -          (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
   1.337 +    fun assign xi (T as TVar (xi', _)) S env =
   1.338 +          if xi = xi' then env
   1.339 +          else env |> meet (T, S) |>> Vartab.update_new (xi, T)
   1.340 +      | assign xi T S (env as (tye, _)) =
   1.341 +          (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
   1.342  
   1.343  
   1.344      (* unification *)
   1.345 @@ -299,16 +257,16 @@
   1.346      fun show_tycon (a, Ts) =
   1.347        quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   1.348  
   1.349 -    fun unif (T1, T2) (tye_idx as (tye, idx)) =
   1.350 -      (case (deref tye T1, deref tye T2) of
   1.351 -        (Param (i, S), T) => assign i T S tye_idx
   1.352 -      | (T, Param (i, S)) => assign i T S tye_idx
   1.353 -      | (PType (a, Ts), PType (b, Us)) =>
   1.354 +    fun unif (T1, T2) (env as (tye, _)) =
   1.355 +      (case pairself (`is_paramT o deref tye) (T1, T2) of
   1.356 +        ((true, TVar (xi, S)), (_, T)) => assign xi T S env
   1.357 +      | ((_, T), (true, TVar (xi, S))) => assign xi T S env
   1.358 +      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   1.359            if a <> b then
   1.360              raise NO_UNIFIER
   1.361                ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
   1.362 -          else fold unif (Ts ~~ Us) tye_idx
   1.363 -      | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
   1.364 +          else fold unif (Ts ~~ Us) env
   1.365 +      | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
   1.366  
   1.367    in unif end;
   1.368  
   1.369 @@ -327,7 +285,7 @@
   1.370  
   1.371      fun prep_output tye bs ts Ts =
   1.372        let
   1.373 -        val (Ts_bTs', ts') = typs_terms_of ctxt tye (Ts @ map snd bs, ts);
   1.374 +        val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
   1.375          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   1.376          fun prep t =
   1.377            let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   1.378 @@ -346,21 +304,20 @@
   1.379  
   1.380      (* main *)
   1.381  
   1.382 -    fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx)
   1.383 -      | inf _ (PFree (_, T)) tye_idx = (T, tye_idx)
   1.384 -      | inf _ (PVar (_, T)) tye_idx = (T, tye_idx)
   1.385 -      | inf bs (PBound i) tye_idx =
   1.386 +    fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
   1.387 +      | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
   1.388 +      | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
   1.389 +      | inf bs (Bound i) tye_idx =
   1.390            (snd (nth bs i handle Subscript => err_loose i), tye_idx)
   1.391 -      | inf bs (PAbs (x, T, t)) tye_idx =
   1.392 +      | inf bs (Abs (x, T, t)) tye_idx =
   1.393            let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   1.394 -          in (PType ("fun", [T, U]), tye_idx') end
   1.395 -      | inf bs (PAppl (t, u)) tye_idx =
   1.396 +          in (T --> U, tye_idx') end
   1.397 +      | inf bs (t $ u) tye_idx =
   1.398            let
   1.399              val (T, tye_idx') = inf bs t tye_idx;
   1.400              val (U, (tye, idx)) = inf bs u tye_idx';
   1.401 -            val V = Param (idx, []);
   1.402 -            val U_to_V = PType ("fun", [U, V]);
   1.403 -            val tye_idx'' = unify ctxt pp (U_to_V, T) (tye, idx + 1)
   1.404 +            val V = mk_param idx [];
   1.405 +            val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
   1.406                handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   1.407            in (V, tye_idx'') end;
   1.408  
   1.409 @@ -381,11 +338,11 @@
   1.410      (*convert to preterms*)
   1.411      val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   1.412      val (ts', (_, _, idx)) =
   1.413 -      fold_map (preterm_of const_type o constrain_vars) ts
   1.414 +      fold_map (prepare_term const_type o constrain_vars) ts
   1.415        (Vartab.empty, Vartab.empty, 0);
   1.416  
   1.417      (*do type inference*)
   1.418 -    val (tye, _) = fold (snd oo infer ctxt) ts' (Inttab.empty, idx);
   1.419 -  in #2 (typs_terms_of ctxt tye ([], ts')) end;
   1.420 +    val (tye, _) = fold (snd oo infer ctxt) ts' (Vartab.empty, idx);
   1.421 +  in #2 (finish ctxt tye ([], ts')) end;
   1.422  
   1.423  end;