diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -1592,9 +1592,6 @@
 
   (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
 
-  (FIXME: @{ML ObjectLogic.full_atomize_tac}, 
-  @{ML ObjectLogic.rulify_tac})
-
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
   (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)