tuned comments: local context is intended according to 06fd1914b902 and documentation for command 'print_interps';
authorwenzelm
Mon, 24 Sep 2018 15:34:19 +0200
changeset 69055 dab89758545c
parent 69054 ba8104f79d7b
child 69056 bc4cc763b0ea
tuned comments: local context is intended according to 06fd1914b902 and documentation for command 'print_interps';
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;