# HG changeset patch
# User wenzelm
# Date 1414682276 -3600
# Node ID 4037bb00d08e06d07843958f6761c2fa033da0bd
# Parent  462ec23aa92f0128971baaf8268716374610d442
tuned spelling;

diff -r 462ec23aa92f -r 4037bb00d08e src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Oct 30 15:57:13 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Oct 30 16:17:56 2014 +0100
@@ -148,7 +148,7 @@
  {thm: thm,         (*the rewrite rule*)
   name: string,     (*name of theorem from which rewrite rule was extracted*)
   lhs: term,        (*the left-hand side*)
-  elhs: cterm,      (*the etac-contracted lhs*)
+  elhs: cterm,      (*the eta-contracted lhs*)
   extra: bool,      (*extra variables outside of elhs*)
   fo: bool,         (*use first-order matching*)
   perm: bool};      (*the rewrite rule is permutative*)