constrain: canonical argument order;
authorwenzelm
Sun Sep 23 22:23:33 2007 +0200 (2007-09-23)
changeset 2468229306b20079b
parent 24681 9d4982db0742
child 24683 c62320337a4e
constrain: canonical argument order;
removed obsolete logicT;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Sun Sep 23 22:23:31 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sun Sep 23 22:23:33 2007 +0200
     1.3 @@ -8,9 +8,8 @@
     1.4  signature TYPE_INFER =
     1.5  sig
     1.6    val anyT: sort -> typ
     1.7 -  val logicT: typ
     1.8    val polymorphicT: typ -> typ
     1.9 -  val constrain: term -> typ -> term
    1.10 +  val constrain: typ -> term -> term
    1.11    val is_param: indexname -> bool
    1.12    val param: int -> string * sort -> typ
    1.13    val paramify_vars: typ -> typ
    1.14 @@ -28,12 +27,11 @@
    1.15  (** type parameters and constraints **)
    1.16  
    1.17  fun anyT S = TFree ("'_dummy_", S);
    1.18 -val logicT = anyT [];
    1.19  
    1.20  (*indicate polymorphic Vars*)
    1.21  fun polymorphicT T = Type ("_polymorphic_", [T]);
    1.22  
    1.23 -fun constrain t T =
    1.24 +fun constrain T t =
    1.25    if T = dummyT then t
    1.26    else Const ("_type_constraint_", T --> T) $ t;
    1.27  
    1.28 @@ -392,8 +390,8 @@
    1.29      (*constrain vars*)
    1.30      val get_type = the_default dummyT o var_type;
    1.31      val constrain_vars = Term.map_aterms
    1.32 -      (fn Free (x, T) => constrain (Free (x, get_type (x, ~1))) T
    1.33 -        | Var (xi, T) => constrain (Var (xi, get_type xi)) T
    1.34 +      (fn Free (x, T) => constrain T (Free (x, get_type (x, ~1)))
    1.35 +        | Var (xi, T) => constrain T (Var (xi, get_type xi))
    1.36          | t => t);
    1.37  
    1.38      (*convert to preterms/typs*)