src/Pure/assumption.ML
changeset 47236 973ab740a25d
parent 46493 7e69b9f3149f
child 54567 cfe53047dc16
--- 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};