diff -r 713629c2b73c -r e6be866b5f5b src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sun Feb 09 17:41:17 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sun Feb 09 17:47:23 2014 +0100
@@ -668,7 +668,7 @@
 
 subsection{*Prime factorizations*}
 
-text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
+(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"