--- a/src/Pure/unify.ML Sun Feb 25 12:59:08 2018 +0100
+++ b/src/Pure/unify.ML Sun Feb 25 15:44:46 2018 +0100
@@ -426,7 +426,7 @@
(*If an argument contains a banned Bound, then it should be deleted.
But if the only path is flexible, this is difficult; the code gives up!
- In %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
+ In \<lambda>x y. ?a x =?= \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
exception CHANGE_FAIL; (*flexible occurrence of banned variable, or other reason to quit*)
@@ -570,7 +570,7 @@
(*Print a tracing message + list of dpairs.
- In t==u print u first because it may be rigid or flexible --
+ In t \<equiv> u print u first because it may be rigid or flexible --
t is always flexible.*)
fun print_dpairs context msg (env, dpairs) =
if Context_Position.is_visible_generic context then
@@ -636,12 +636,12 @@
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
- Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
- Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
+ Unifies ?f t1 ... rm with ?g u1 ... un by ?f -> \<lambda>x1...xm. ?a, ?g -> \<lambda>x1...xn. ?a
+ Unfortunately, unifies ?f t u with ?g t u by ?f, ?g -> \<lambda>x y. ?a,
though just ?g->?f is a more general unifier.
Unlike Huet (1975), does not smash together all variables of same type --
requires more work yet gives a less general unifier (fewer variables).
- Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
+ Handles ?f t1 ... rm with ?f u1 ... um to avoid multiple updates. *)
fun smash_flexflex1 (t, u) env : Envir.env =
let
val vT as (v, T) = var_head_of (env, t)