# HG changeset patch
# User lcp
# Date 782556108 -3600
# Node ID 112cf8574cf1d06fd0cd6530bfda2dd4f7f8028b
# Parent  1e8fea151d2ebd630856d3f4f10ee1ccf4bd8ee8
FOL/ex/cla/58: slightly shorter proof

diff -r 1e8fea151d2e -r 112cf8574cf1 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Wed Oct 19 09:39:23 1994 +0100
+++ b/src/FOL/ex/cla.ML	Wed Oct 19 09:41:48 1994 +0100
@@ -468,8 +468,7 @@
 
 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
 goal FOL.thy "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
-val f_cong = read_instantiate [("t","f")] subst_context;
-by (fast_tac (FOL_cs addIs [f_cong]) 1);
+by (fast_tac (FOL_cs addEs [subst_context]) 1);
 result();
 
 writeln"Problem 59";