--- a/src/Pure/logic.ML Thu Oct 21 14:47:48 1993 +0100
+++ b/src/Pure/logic.ML Thu Oct 21 14:56:12 1993 +0100
@@ -51,8 +51,8 @@
(** equality **)
-(*Make an equality. DOES NOT CHECK TYPE OF u! *)
-fun mk_equals(t,u) = equals(type_of t) $ t $ u;
+(*Make an equality.*)
+fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
fun dest_equals (Const("==",_) $ t $ u) = (t,u)
| dest_equals t = raise TERM("dest_equals", [t]);
@@ -92,8 +92,8 @@
(** flex-flex constraints **)
-(*Make a constraint. DOES NOT CHECK TYPE OF u! *)
-fun mk_flexpair(t,u) = flexpair(type_of t) $ t $ u;
+(*Make a constraint.*)
+fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u;
fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u)
| dest_flexpair t = raise TERM("dest_flexpair", [t]);