# HG changeset patch
# User wenzelm
# Date 1365015368 -7200
# Node ID f836617331431dbca95926176e01e1bc5b72c13b
# Parent  92fda7beace45be0e693108e88241a87298a5b66
updated comment to 46b90bbc370d;

diff -r 92fda7beace4 -r f83661733143 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 03 20:38:50 2013 +0200
+++ b/src/Pure/thm.ML	Wed Apr 03 20:56:08 2013 +0200
@@ -1377,7 +1377,7 @@
   in addprfs asms 1 end;
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
-  Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
+  Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*)
 fun eq_assumption i state =
   let
     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;