src/HOL/thy_data.ML

--- a/src/HOL/thy_data.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/HOL/thy_data.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -106,7 +106,7 @@
 end;
 
 (*Must be redefined in order to refer to the new instance of bind_thm
-  created by init_thy_reader.*)
+  created by init_thy_reader.*)		(* FIXME: move *)
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())