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);