src/Pure/type_infer.ML
changeset 39288 f1ae2493d93f
parent 39287 d30be6791038
child 39289 92b50c8bb67b
     1.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  sig
     1.5    val anyT: sort -> typ
     1.6    val polymorphicT: typ -> typ
     1.7 -  val constrain: typ -> term -> term
     1.8    val is_param: indexname -> bool
     1.9    val param: int -> string * sort -> typ
    1.10    val paramify_vars: typ -> typ
    1.11 @@ -31,8 +30,6 @@
    1.12  (*indicate polymorphic Vars*)
    1.13  fun polymorphicT T = Type ("_polymorphic_", [T]);
    1.14  
    1.15 -val constrain = Syntax.type_constraint;
    1.16 -
    1.17  
    1.18  (* type inference parameters -- may get instantiated *)
    1.19  
    1.20 @@ -418,8 +415,8 @@
    1.21      (*constrain vars*)
    1.22      val get_type = the_default dummyT o var_type;
    1.23      val constrain_vars = Term.map_aterms
    1.24 -      (fn Free (x, T) => constrain T (Free (x, get_type (x, ~1)))
    1.25 -        | Var (xi, T) => constrain T (Var (xi, get_type xi))
    1.26 +      (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
    1.27 +        | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
    1.28          | t => t);
    1.29  
    1.30      (*convert to preterms*)