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;