src/Pure/Isar/locale.ML
changeset 56141 c06202417c4a
parent 56140 ed92ce2ac88e
child 56204 f70e69208a8c
--- a/src/Pure/Isar/locale.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -561,7 +561,7 @@
           (* Registrations *)
           (fn thy =>
             fold_rev (fn (_, morph) =>
-              snd o Attrib.global_notes kind (Element.transform_facts morph facts))  (* FIXME background_notes *)
+              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
             (registrations_of (Context.Theory thy) loc) thy));