Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
authorwenzelm
Mon Sep 13 12:42:08 2010 +0200 (2010-09-13)
changeset 392956e8b0672c6a2
parent 39294 27fae73fe769
child 39296 e275d581a218
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
Type_Infer.fixate_params: full Proof.context;
src/Pure/Isar/proof_context.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 13 11:35:55 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 13 12:42:08 2010 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4  
     1.5  fun prepare_patterns ctxt =
     1.6    let val Mode {pattern, ...} = get_mode ctxt in
     1.7 -    Type_Infer.fixate_params (Variable.names_of ctxt) #>
     1.8 +    Type_Infer.fixate_params ctxt #>
     1.9      pattern ? Variable.polymorphic ctxt #>
    1.10      (map o Term.map_types) (prepare_patternT ctxt) #>
    1.11      (if pattern then prepare_dummies else map (check_dummies ctxt))
     2.1 --- a/src/Pure/type_infer.ML	Mon Sep 13 11:35:55 2010 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Mon Sep 13 12:42:08 2010 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4    val param: int -> string * sort -> typ
     2.5    val paramify_vars: typ -> typ
     2.6    val paramify_dummies: typ -> int -> typ * int
     2.7 -  val fixate_params: Name.context -> term list -> term list
     2.8 +  val fixate_params: Proof.context -> term list -> term list
     2.9    val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    2.10      term list -> term list
    2.11  end;
    2.12 @@ -54,7 +54,7 @@
    2.13        | paramify T maxidx = (T, maxidx);
    2.14    in paramify end;
    2.15  
    2.16 -fun fixate_params name_context ts =
    2.17 +fun fixate_params ctxt ts =
    2.18    let
    2.19      fun subst_param (xi, S) (inst, used) =
    2.20        if is_param xi then
    2.21 @@ -63,8 +63,8 @@
    2.22            val used' = Name.declare a used;
    2.23          in (((xi, S), TFree (a, S)) :: inst, used') end
    2.24        else (inst, used);
    2.25 -    val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
    2.26 -    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
    2.27 +    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
    2.28 +    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
    2.29    in (map o map_types) (Term_Subst.instantiateT inst) ts end;
    2.30  
    2.31  
    2.32 @@ -188,7 +188,6 @@
    2.33      val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
    2.34      val names = Name.invents used ("?" ^ Name.aT) (length parms);
    2.35      val tab = Vartab.make (parms ~~ names);
    2.36 -    val idx = Variable.maxidx_of ctxt + 1;
    2.37  
    2.38      fun finish_typ T =
    2.39        (case deref tye T of
    2.40 @@ -197,7 +196,7 @@
    2.41        | U as TVar (xi, S) =>
    2.42            (case Vartab.lookup tab xi of
    2.43              NONE => U
    2.44 -          | SOME a => TVar ((a, idx), S)));
    2.45 +          | SOME a => TVar ((a, 0), S)));
    2.46    in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
    2.47  
    2.48