--- a/src/Pure/type.ML Wed Jul 06 12:49:56 1994 +0200
+++ b/src/Pure/type.ML Wed Jul 06 12:51:27 1994 +0200
@@ -51,6 +51,7 @@
-> (indexname * typ) list
val unify: type_sig -> (typ * typ) * (indexname * typ) list
-> (indexname * typ) list
+ val raw_unify: typ * typ -> bool
val varifyT: typ -> typ
val varify: term * string list -> term
exception TUNIFY
@@ -866,6 +867,13 @@
in unif end;
+(* raw_unify (ignores sorts) *)
+
+fun raw_unify (ty1, ty2) =
+ (unify tsig0 ((rem_sorts ty1, rem_sorts ty2), []); true)
+ handle TUNIFY => false;
+
+
(*Type inference for polymorphic term*)
fun infer tsig =
let fun inf(Ts, Const (_, T), tye) = (T, tye)