# HG changeset patch
# User wenzelm
# Date 1237300482 -3600
# Node ID deddb8a1516fa5edb1d22a5d06d7abceb937fe51
# Parent  e99c5466af9294a7d2cb819ff7b6934120505b1a
tuned comment;

diff -r e99c5466af92 -r deddb8a1516f src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Mar 17 14:14:25 2009 +0100
+++ b/src/Pure/more_thm.ML	Tue Mar 17 15:34:42 2009 +0100
@@ -208,15 +208,12 @@
   in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end;
 
 
-(* lists of theorems in canonical order *)
+(* collections of theorems in canonical order *)
 
 val add_thm = update eq_thm_prop;
 val del_thm = remove eq_thm_prop;
 val merge_thms = merge eq_thm_prop;
 
-
-(* indexed collections *)
-
 val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of;
 val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of;