# HG changeset patch
# User blanchet
# Date 1381300116 -7200
# Node ID c2782ec22cc6841af82423dbea87dc9e4c9dedb4
# Parent  824db6ab33391ec2c80554bc1798a186826e43e6
added TODO

diff -r 824db6ab3339 -r c2782ec22cc6 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 08:12:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 08:28:36 2013 +0200
@@ -309,6 +309,7 @@
 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
 fun backquote_thm ctxt = backquote_term ctxt o prop_of
 
+(* TODO: rewrite to use nets and/or to reuse existing data structures *)
 fun clasimpset_rule_table_of ctxt =
   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
     if length simps >= max_simps_for_clasimpset then