# 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)