diff -r 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 21:11:15 2009 +0100
@@ -14,7 +14,7 @@
 structure InductiveRealizer : INDUCTIVE_REALIZER =
 struct
 
-(* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
+(* FIXME: Local_Theory.note should return theorems with proper names! *)  (* FIXME ?? *)
 fun name_of_thm thm =
   (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
       [Thm.proof_of thm] [] of