src/Pure/theory.ML
changeset 68484 59793df7f853
parent 68482 cb84beb84ca9
child 69289 bf6937af7fe8
--- a/src/Pure/theory.ML	Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Pure/theory.ML	Fri Jun 22 20:31:49 2018 +0200
@@ -143,7 +143,7 @@
               Completion.make (name, pos)
                 (fn completed =>
                   map (Context.theory_name' long) (ancestors_of thy)
-                  |> filter completed
+                  |> filter (completed o Long_Name.base_name)
                   |> sort_strings
                   |> map (fn a => (a, (Markup.theoryN, a))));
             val report = Markup.markup_report (Completion.reported_text completion);