# HG changeset patch
# User wenzelm
# Date 1333200095 -7200
# Node ID 973ab740a25d2bd1983507ffc0eeb3b518029c0c
# Parent  a92d3620e1566ae860e5261575246af2003d7797
tuned comment;

diff -r a92d3620e156 -r 973ab740a25d src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Mar 30 21:08:00 2012 +0200
+++ b/src/Pure/assumption.ML	Sat Mar 31 15:21:35 2012 +0200
@@ -56,7 +56,7 @@
 
 datatype data = Data of
  {assms: (export * cterm list) list,    (*assumes: A ==> _*)
-  prems: thm list};                     (*prems: A |- A*)
+  prems: thm list};                     (*prems: A |- norm_hhf A*)
 
 fun make_data (assms, prems) = Data {assms = assms, prems = prems};