src/Pure/theory.ML
changeset 69289 bf6937af7fe8
parent 68484 59793df7f853
child 69886 0cb8753bdb50
--- a/src/Pure/theory.ML	Mon Nov 12 14:02:33 2018 +0100
+++ b/src/Pure/theory.ML	Mon Nov 12 15:14:12 2018 +0100
@@ -139,15 +139,14 @@
       Context.get_theory long thy name
         handle ERROR msg =>
           let
-            val completion =
-              Completion.make (name, pos)
+            val completion_report =
+              Completion.make_report (name, pos)
                 (fn completed =>
                   map (Context.theory_name' long) (ancestors_of thy)
                   |> 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);
-          in error (msg ^ Position.here pos ^ report) end;
+          in error (msg ^ Position.here pos ^ completion_report) end;
     val _ = Context_Position.report ctxt pos (get_markup thy');
   in thy' end;