new comments explaining abandoned change
authorlcp
Wed Oct 19 09:48:13 1994 +0100 (1994-10-19)
changeset 6467928c9760667
parent 645 77474875da92
child 647 fb7345cccddc
new comments explaining abandoned change
src/Provers/hypsubst.ML
src/Pure/unify.ML
     1.1 --- a/src/Provers/hypsubst.ML	Wed Oct 19 09:44:31 1994 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Oct 19 09:48:13 1994 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title: 	Provers/hypsubst
     1.5      ID:         $Id$
     1.6 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10  Martin Coen's tactic for substitution in the hypotheses
    1.11 @@ -49,6 +49,7 @@
    1.12  
    1.13  (*It's not safe to substitute for a constant; consider 0=1.
    1.14    It's not safe to substitute for x=t[x] since x is not eliminated.
    1.15 +  It's not safe to substitute for a Var; what if it appears in other goals?
    1.16    It's not safe to substitute for a variable free in the premises,
    1.17      but how could we check for this?*)
    1.18  fun inspect_pair bnd (t,u) =
     2.1 --- a/src/Pure/unify.ML	Wed Oct 19 09:44:31 1994 +0100
     2.2 +++ b/src/Pure/unify.ML	Wed Oct 19 09:48:13 1994 +0100
     2.3 @@ -7,6 +7,10 @@
     2.4  
     2.5  Potential problem: type of Vars is often ignored, so two Vars with same
     2.6  indexname but different types can cause errors!
     2.7 +
     2.8 +Types as well as terms are unified.  The outermost functions assume the
     2.9 +terms to be unified already have the same type.  In resolution, this is
    2.10 +assured because both have type "prop".
    2.11  *)
    2.12  
    2.13  
    2.14 @@ -303,7 +307,10 @@
    2.15  
    2.16  (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
    2.17    Does not perform assignments for flex-flex pairs:
    2.18 -    may create nonrigid paths, which prevent other assignments*)
    2.19 +    may create nonrigid paths, which prevent other assignments.
    2.20 +  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
    2.21 +    do so caused numerous problems with no compensating advantage.
    2.22 +*)
    2.23  fun SIMPL0 (dp0, (env,flexflex,flexrigid))
    2.24  	: Envir.env * dpair list * dpair list =
    2.25      let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);