src/HOL/Tools/Quotient/quotient_tacs.ML

 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
 fun atomize_thm thm =
 let
-  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
+  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
   val thm'' = Object_Logic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']
 end