# HG changeset patch
# User lcp
# Date 782556493 -3600
# Node ID 7928c97606679b14192ce9a224acda3b6570606f
# Parent  77474875da92c66640c18946e96e47e94a3200f8
new comments explaining abandoned change

diff -r 77474875da92 -r 7928c9760667 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Oct 19 09:44:31 1994 +0100
+++ b/src/Provers/hypsubst.ML	Wed Oct 19 09:48:13 1994 +0100
@@ -1,6 +1,6 @@
 (*  Title: 	Provers/hypsubst
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Martin Coen's tactic for substitution in the hypotheses
@@ -49,6 +49,7 @@
 
 (*It's not safe to substitute for a constant; consider 0=1.
   It's not safe to substitute for x=t[x] since x is not eliminated.
+  It's not safe to substitute for a Var; what if it appears in other goals?
   It's not safe to substitute for a variable free in the premises,
     but how could we check for this?*)
 fun inspect_pair bnd (t,u) =
diff -r 77474875da92 -r 7928c9760667 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Oct 19 09:44:31 1994 +0100
+++ b/src/Pure/unify.ML	Wed Oct 19 09:48:13 1994 +0100
@@ -7,6 +7,10 @@
 
 Potential problem: type of Vars is often ignored, so two Vars with same
 indexname but different types can cause errors!
+
+Types as well as terms are unified.  The outermost functions assume the
+terms to be unified already have the same type.  In resolution, this is
+assured because both have type "prop".
 *)
 
 
@@ -303,7 +307,10 @@
 
 (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   Does not perform assignments for flex-flex pairs:
-    may create nonrigid paths, which prevent other assignments*)
+    may create nonrigid paths, which prevent other assignments.
+  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
+    do so caused numerous problems with no compensating advantage.
+*)
 fun SIMPL0 (dp0, (env,flexflex,flexrigid))
 	: Envir.env * dpair list * dpair list =
     let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);