src/Pure/unify.ML
changeset 646 7928c9760667
parent 0 a5a9c433f639
child 651 4b0455fbcc49
     1.1 --- a/src/Pure/unify.ML	Wed Oct 19 09:44:31 1994 +0100
     1.2 +++ b/src/Pure/unify.ML	Wed Oct 19 09:48:13 1994 +0100
     1.3 @@ -7,6 +7,10 @@
     1.4  
     1.5  Potential problem: type of Vars is often ignored, so two Vars with same
     1.6  indexname but different types can cause errors!
     1.7 +
     1.8 +Types as well as terms are unified.  The outermost functions assume the
     1.9 +terms to be unified already have the same type.  In resolution, this is
    1.10 +assured because both have type "prop".
    1.11  *)
    1.12  
    1.13  
    1.14 @@ -303,7 +307,10 @@
    1.15  
    1.16  (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
    1.17    Does not perform assignments for flex-flex pairs:
    1.18 -    may create nonrigid paths, which prevent other assignments*)
    1.19 +    may create nonrigid paths, which prevent other assignments.
    1.20 +  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
    1.21 +    do so caused numerous problems with no compensating advantage.
    1.22 +*)
    1.23  fun SIMPL0 (dp0, (env,flexflex,flexrigid))
    1.24  	: Envir.env * dpair list * dpair list =
    1.25      let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);