src/Pure/Thy/thy_output.ML

   let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
-fun pretty_theory ctxt name =
-  (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
+fun pretty_theory ctxt (name, pos) =
+  (case find_first (fn thy => Context.theory_name thy = name)
+      (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
+    NONE => error ("No ancestor theory " ^ quote name ^ Position.str_of pos)
+  | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
 
 
 (* default output *)
 
 val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;

     basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
     basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
     basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
     basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
     basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
-    basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
+    basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory #>
     basic_entities_style (Binding.name "thm_style")
       (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
     basic_entity (Binding.name "term_style")
       (Term_Style.parse_bare -- Args.term) pretty_term_style));