# HG changeset patch
# User wenzelm
# Date 1537796059 -7200
# Node ID dab89758545cc3c99871b7d8fff39bddb1d3c955
# Parent  ba8104f79d7bd759f24a26715040d174f806d33d
tuned comments: local context is intended according to 06fd1914b902 and documentation for command 'print_interps';

diff -r ba8104f79d7b -r dab89758545c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 15:31:43 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 15:34:19 2018 +0200
@@ -735,7 +735,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val name = check thy raw_name;
   in
-    (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
+    (case registrations_of (Context.Proof ctxt) name of
       [] => Pretty.str "no interpretations"
     | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)))
   end |> Pretty.writeln;