--- 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) =
--- 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);