# HG changeset patch
# User wenzelm
# Date 1272654657 -7200
# Node ID ca42a56e3b14976004c496a1fb987a87c42105c2
# Parent  c798ad2c92287252f4fb1166443d13c122e74c00
removed some old comments;

diff -r c798ad2c9228 -r ca42a56e3b14 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 30 09:54:04 2010 -0700
+++ b/src/FOL/simpdata.ML	Fri Apr 30 21:10:57 2010 +0200
@@ -35,10 +35,6 @@
   [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
    ("All", [@{thm spec}]), ("True", []), ("False", [])];
 
-(* ###FIXME: move to simplifier.ML
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-*)
-(* ###FIXME: move to simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of