# HG changeset patch
# User wenzelm
# Date 773491887 -7200
# Node ID 382b5368ec215870faa9bbdf6a9ace7d48a336f6
# Parent  75ac32497f09b5f5a90940f7edc4aff5ca6807c7
added raw_unify;

diff -r 75ac32497f09 -r 382b5368ec21 src/Pure/type.ML
--- 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)