clarified signature;

--- a/src/Pure/ML/ml_antiquotations.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -46,13 +46,14 @@
 
   ML_Antiquotation.value \<^binding>\<open>theory\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
-      (Theory.check ctxt (name, pos);
-       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
+      (Theory.check {long = false} ctxt (name, pos);
+       "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
+        ML_Syntax.print_string name))
     || Scan.succeed "Proof_Context.theory_of ML_context") #>
 
   ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
-      (Theory.check ctxt (name, pos);
+      (Theory.check {long = false} ctxt (name, pos);
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>
 

--- a/src/Pure/Pure.thy	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/Pure.thy	Thu Jun 21 14:49:21 2018 +0200
@@ -1269,7 +1269,7 @@
             val thy = Toplevel.theory_of st;
             val ctxt = Toplevel.context_of st;
             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
-            val check = Theory.check ctxt;
+            val check = Theory.check {long = false} ctxt;
           in
             Thm_Deps.unused_thms
               (case opt_range of

--- a/src/Pure/Thy/document_antiquotations.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -60,7 +60,8 @@
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
 
-fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
+fun pretty_theory ctxt (name, pos) =
+  (Theory.check {long = false} ctxt (name, pos); Pretty.str name);
 
 val basic_entity = Thy_Output.antiquotation_pretty_source;
 

--- a/src/Pure/Thy/thy_output.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -246,7 +246,7 @@
   let
     val ctxt' =
       Toplevel.presentation_context state'
-        handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN);
+        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
     val present = fold (fn (tok, (flag, 0)) =>
         fold cons (present_token ctxt' tok)
         #> cons (Latex.string flag)

--- a/src/Pure/Tools/thm_deps.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -27,7 +27,7 @@
             val session =
               (case prefix of
                 a :: _ =>
-                  (case try (Context.get_theory thy) a of
+                  (case try (Context.get_theory {long = false} thy) a of
                     SOME thy =>
                       (case Present.theory_qualifier thy of
                         "" => []

--- a/src/Pure/Tools/thy_deps.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -36,6 +36,6 @@
     let val thy0 = Proof_Context.theory_of ctxt
     in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
 
-val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
+val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false});
 
 end;

--- a/src/Pure/context.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/context.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -37,11 +37,11 @@
   val theory_id_name: theory_id -> string
   val theory_long_name: theory -> string
   val theory_name: theory -> string
+  val theory_name': {long: bool} -> theory -> string
   val PureN: string
   val pretty_thy: theory -> Pretty.T
   val pretty_abbrev_thy: theory -> Pretty.T
-  val get_theory: theory -> string -> theory
-  val this_theory: theory -> string -> theory
+  val get_theory: {long: bool} -> theory -> string -> theory
   val eq_thy_id: theory_id * theory_id -> bool
   val eq_thy: theory * theory -> bool
   val proper_subthy_id: theory_id * theory_id -> bool
@@ -160,6 +160,7 @@
 val theory_id_name = Long_Name.base_name o theory_id_long_name;
 val theory_long_name = #name o history_of;
 val theory_name = Long_Name.base_name o theory_long_name;
+fun theory_name' {long} = if long then theory_long_name else theory_name;
 
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;
@@ -191,18 +192,14 @@
     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   in Pretty.str_list "{" "}" abbrev end;
 
-fun get_theory thy name =
-  if theory_name thy <> name then
-    (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
+fun get_theory long thy name =
+  if theory_name' long thy <> name then
+    (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
       SOME thy' => thy'
     | NONE => error ("Unknown ancestor theory " ^ quote name))
   else if #stage (history_of thy) = finished then thy
   else error ("Unfinished theory " ^ quote name);
 
-fun this_theory thy name =
-  if theory_name thy = name then thy
-  else get_theory thy name;
-
 
 (* build ids *)
 
@@ -472,7 +469,7 @@
 struct
   fun theory_of (Proof.Context (_, thy)) = thy;
   fun init_global thy = Proof.Context (init_data thy, thy);
-  fun get_global thy name = init_global (get_theory thy name);
+  fun get_global thy name = init_global (get_theory {long = false} thy name);
 end;
 
 structure Proof_Data =

--- a/src/Pure/theory.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Pure/theory.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -14,7 +14,7 @@
   val install_pure: theory -> unit
   val get_pure: unit -> theory
   val get_markup: theory -> Markup.T
-  val check: Proof.context -> string * Position.T -> theory
+  val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
   val axioms_of: theory -> (string * term) list
@@ -132,17 +132,17 @@
   let val {pos, id, ...} = rep_theory thy
   in theory_markup false (Context.theory_name thy) id pos end;
 
-fun check ctxt (name, pos) =
+fun check long ctxt (name, pos) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val thy' =
-      Context.get_theory thy name
+      Context.get_theory long thy name
         handle ERROR msg =>
           let
             val completion =
               Completion.make (name, pos)
                 (fn completed =>
-                  map Context.theory_name (ancestors_of thy)
+                  map (Context.theory_name' long) (ancestors_of thy)
                   |> filter completed
                   |> sort_strings
                   |> map (fn a => (a, (Markup.theoryN, a))));

--- a/src/Tools/Code/code_thingol.ML	Thu Jun 21 14:29:44 2018 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Jun 21 14:49:21 2018 +0200
@@ -942,6 +942,10 @@
 fun read_const_exprs_internal ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
+    fun this_theory name =
+      if Context.theory_name thy = name then thy
+      else Context.get_theory {long = false} thy name;
+
     fun consts_of thy' =
       fold (fn (c, (_, NONE)) => cons c | _ => I)
         (#constants (Consts.dest (Sign.consts_of thy'))) []
@@ -954,7 +958,7 @@
         SOME "_" => ([], consts_of thy)
       | SOME s =>
           if String.isSuffix "._" s
-          then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
+          then ([], consts_of_select (this_theory (unsuffix "._" s)))
           else ([Code.read_const thy str], [])
       | NONE => ([Code.read_const thy str], []));
   in apply2 flat o split_list o map read_const_expr end;