diff -r f4ed4d940d44 -r 3b99944136ef src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Sun Jan 21 16:43:46 2007 +0100
+++ b/src/HOL/ex/Binary.thy	Sun Jan 21 16:43:47 2007 +0100
@@ -127,7 +127,7 @@
   val plus = nat_op "HOL.plus";
   val mult = nat_op "HOL.times";
 
-  fun prove ctxt prop =  (* FIXME avoid re-certification *)
+  fun prove ctxt prop =
     Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));