1.1 --- a/src/Pure/logic.ML	Thu Oct 21 14:47:48 1993 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Oct 21 14:56:12 1993 +0100
     1.3 @@ -51,8 +51,8 @@
     1.4  
     1.5  (** equality **)
     1.6  
     1.7 -(*Make an equality.  DOES NOT CHECK TYPE OF u! *)
     1.8 -fun mk_equals(t,u) = equals(type_of t) $ t $ u;
     1.9 +(*Make an equality.*)
    1.10 +fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    1.11  
    1.12  fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    1.13    | dest_equals t = raise TERM("dest_equals", [t]);
    1.14 @@ -92,8 +92,8 @@
    1.15  
    1.16  (** flex-flex constraints **)
    1.17  
    1.18 -(*Make a constraint.  DOES NOT CHECK TYPE OF u! *)
    1.19 -fun mk_flexpair(t,u) = flexpair(type_of t) $ t $ u;
    1.20 +(*Make a constraint.*)
    1.21 +fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u;
    1.22  
    1.23  fun dest_flexpair (Const("=?=",_) $ t $ u)  =  (t,u)
    1.24    | dest_flexpair t = raise TERM("dest_flexpair", [t]);