src/Pure/unify.ML
changeset 1505 14f4c55bbe9a
parent 1460 5a6f2aabd538
child 2140 eaa7ab39889d
     1.1 --- a/src/Pure/unify.ML	Fri Feb 16 13:49:40 1996 +0100
     1.2 +++ b/src/Pure/unify.ML	Fri Feb 16 13:55:29 1996 +0100
     1.3 @@ -15,10 +15,7 @@
     1.4  
     1.5  
     1.6  signature UNIFY = 
     1.7 -sig
     1.8 -  structure Sign: SIGN
     1.9 -  structure Envir : ENVIR
    1.10 -  structure Sequence : SEQUENCE
    1.11 +  sig
    1.12    (*references for control and tracing*)
    1.13    val trace_bound: int ref
    1.14    val trace_simp: bool ref
    1.15 @@ -31,20 +28,11 @@
    1.16  	-> (Envir.env Sequence.seq)
    1.17    val unifiers: Sign.sg * Envir.env * ((term*term)list)
    1.18  	-> (Envir.env * (term * term)list) Sequence.seq
    1.19 -end;
    1.20 +  end;
    1.21  
    1.22 -functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
    1.23 -                  and Pattern:PATTERN
    1.24 -                  sharing type Sign.sg = Pattern.sg
    1.25 -                  and     type Envir.env = Pattern.env)
    1.26 -	: UNIFY = 
    1.27 +structure Unify	: UNIFY = 
    1.28  struct
    1.29  
    1.30 -structure Sign = Sign;
    1.31 -structure Envir = Envir;
    1.32 -structure Sequence = Sequence;
    1.33 -structure Pretty = Sign.Syntax.Pretty;
    1.34 -
    1.35  (*Unification options*)
    1.36  
    1.37  val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
    1.38 @@ -243,10 +231,10 @@
    1.39  
    1.40  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.41    if T=U then env
    1.42 -  else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr)))
    1.43 +  else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr)))
    1.44                                                  maxidx iTs (U,T)
    1.45         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.46 -       handle Sign.Type.TUNIFY => raise CANTUNIFY;
    1.47 +       handle Type.TUNIFY => raise CANTUNIFY;
    1.48  
    1.49  fun test_unify_types(args as (T,U,_)) =
    1.50  let val sot = Sign.string_of_typ (!sgr);