diff -r b8a94ed1646e -r c422128d3889 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed May 23 15:57:12 2012 +0200
+++ b/src/Provers/clasimp.ML	Wed May 23 16:22:27 2012 +0200
@@ -173,14 +173,12 @@
 
 (* basic combinations *)
 
-fun fast_simp_tac ctxt i =
-  let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
-  in Classical.fast_tac (addss ctxt) i end;
-
 val fast_force_tac = Classical.fast_tac o addss;
 val slow_simp_tac = Classical.slow_tac o addss;
 val best_simp_tac = Classical.best_tac o addss;
 
+
+
 (** concrete syntax **)
 
 (* attributes *)
@@ -221,7 +219,6 @@
 
 val clasimp_setup =
   Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
-  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
   Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
   Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
   Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>