# HG changeset patch
# User lcp
# Date 751211772 -3600
# Node ID 0bbe5d86cb38d9489d9c4e28f7867d0e47ca2a23
# Parent  b1349b598560179ab82cfce55f55b35fddd4bbff
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...

diff -r b1349b598560 -r 0bbe5d86cb38 src/Pure/logic.ML
--- 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]);