src/Pure/type_infer.ML
changeset 62958 b41c1cb5e251
parent 53672 df8068269e90
child 64556 851ae0e7b09c
     1.1 --- a/src/Pure/type_infer.ML	Tue Apr 12 13:49:37 2016 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Apr 12 14:38:57 2016 +0200
     1.3 @@ -16,7 +16,8 @@
     1.4    val paramify_vars: typ -> typ
     1.5    val deref: typ Vartab.table -> typ -> typ
     1.6    val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
     1.7 -  val fixate: Proof.context -> term list -> term list
     1.8 +  val object_logic: bool Config.T
     1.9 +  val fixate: Proof.context -> bool -> term list -> term list
    1.10  end;
    1.11  
    1.12  structure Type_Infer: TYPE_INFER =
    1.13 @@ -99,14 +100,22 @@
    1.14  
    1.15  (* fixate -- introduce fresh type variables *)
    1.16  
    1.17 -fun fixate ctxt ts =
    1.18 +val object_logic =
    1.19 +  Config.bool (Config.declare ("Type_Infer.object_logic", @{here}) (K (Config.Bool true)));
    1.20 +
    1.21 +fun fixate ctxt pattern ts =
    1.22    let
    1.23 +    val base_sort = Object_Logic.get_base_sort ctxt;
    1.24 +    val improve_sort =
    1.25 +      if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
    1.26 +      then fn [] => the base_sort | S => S else I;
    1.27 +
    1.28      fun subst_param (xi, S) (inst, used) =
    1.29        if is_param xi then
    1.30          let
    1.31            val [a] = Name.invent used Name.aT 1;
    1.32            val used' = Name.declare a used;
    1.33 -        in (((xi, S), TFree (a, S)) :: inst, used') end
    1.34 +        in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
    1.35        else (inst, used);
    1.36      val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
    1.37      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);