# HG changeset patch
# User wenzelm
# Date 1429210441 -7200
# Node ID f5c4b49c8c9a36f74187bac245d479eb588c4e0e
# Parent  0a064330a885b8681884b14460fa2e1a3749da1f# Parent  2ce2e0358e91ed635ef9e0d2b6c80be6db12216d
merged;

diff -r 0a064330a885 -r f5c4b49c8c9a NEWS
--- a/NEWS	Thu Apr 16 15:55:55 2015 +0200
+++ b/NEWS	Thu Apr 16 20:54:01 2015 +0200
@@ -74,10 +74,11 @@
 * Less waste of vertical space via negative line spacing (see Global
 Options / Text Area).
 
-* Improved graphview panel (with optional output of PNG or PDF)
-supersedes the old graph browser from 1996, but the latter remains
-available for some time as a fall-back. The old browser is still
-required for the massive graphs produced by 'thm_deps', for example.
+* Improved graphview panel with optional output of PNG or PDF, for
+display of 'thy_deps', 'locale_deps', 'class_deps' etc.
+
+* Command 'thy_deps' allows optional bounds, analogously to
+'class_deps'.
 
 * Improved scheduling for asynchronous print commands (e.g. provers
 managed by the Sledgehammer panel) wrt. ongoing document processing.
@@ -397,6 +398,9 @@
 derivatives) instead, which is not affected by the change. Potential
 INCOMPATIBILITY in rare applications of Name_Space.intern.
 
+* Subtle change of error semantics of Toplevel.proof_of: regular user
+ERROR instead of internal Toplevel.UNDEF.
+
 * Basic combinators map, fold, fold_map, split_list, apply are available
 as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
 
diff -r 0a064330a885 -r f5c4b49c8c9a src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy	Thu Apr 16 20:54:01 2015 +0200
@@ -62,7 +62,7 @@
   for an empty toplevel state.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
-  state if available, otherwise it raises @{ML Toplevel.UNDEF}.
+  state if available, otherwise it raises an error.
 
   \end{description}
 \<close>
diff -r 0a064330a885 -r f5c4b49c8c9a src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 20:54:01 2015 +0200
@@ -25,6 +25,7 @@
   \begin{matharray}{rcl}
     @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
     @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
+    @{command_def "thy_deps"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow>"} \\
   \end{matharray}
 
   Isabelle/Isar theories are defined via theory files, which consist of an
@@ -64,6 +65,10 @@
     ;
     keyword_decls: (@{syntax string} +)
       ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
+    ;
+    @@{command thy_deps} (thy_bounds thy_bounds?)?
+    ;
+    thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'
   \<close>}
 
   \begin{description}
@@ -104,6 +109,12 @@
   @{keyword "begin"} that needs to be matched by @{command (local)
   "end"}, according to the usual rules for nested blocks.
 
+  \item @{command thy_deps} visualizes the theory hierarchy as a directed
+  acyclic graph. By default, all imported theories are shown, taking the
+  base session as a starting point. Alternatively, it is possibly to
+  restrict the full theory graph by giving bounds, analogously to
+  @{command_ref class_deps}.
+
   \end{description}
 \<close>
 
@@ -948,8 +959,9 @@
     ;
     @@{command subclass} @{syntax nameref}
     ;
-    @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
-      ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
+    @@{command class_deps} (class_bounds class_bounds?)?
+    ;
+    class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
   \<close>}
 
   \begin{description}
@@ -1012,11 +1024,13 @@
   \item @{command "print_classes"} prints all classes in the current
   theory.
 
-  \item @{command "class_deps"} visualizes all classes and their
-  subclass relations as a Hasse diagram.  An optional first argument
-  constrains the set of classes to all subclasses of at least one given
-  sort, an optional second rgument to all superclasses of at least one given
-  sort.
+  \item @{command "class_deps"} visualizes classes and their subclass
+  relations as a directed acyclic graph. By default, all classes from the
+  current theory context are show. This may be restricted by optional bounds
+  as follows: @{command "class_deps"}~@{text upper} or @{command
+  "class_deps"}~@{text "upper lower"}. A class is visualized, iff it is a
+  subclass of some sort from @{text upper} and a superclass of some sort
+  from @{text lower}.
 
   \item @{method intro_classes} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Library/refute.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -2969,7 +2969,6 @@
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
-        Toplevel.unknown_proof o
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 16 20:54:01 2015 +0200
@@ -441,8 +441,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_orders}
     "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_structures o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
 
 
 (* tactics *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -377,7 +377,6 @@
   Outer_Syntax.command @{command_keyword nitpick}
     "try to find a counterexample for a given subgoal using Nitpick"
     (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
-      Toplevel.unknown_proof o
       Toplevel.keep (fn state =>
         ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
           (Toplevel.proof_of state)))))
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -359,7 +359,6 @@
   end
 
 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
-  Toplevel.unknown_proof o
   Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
 
 fun string_of_raw_param (key, values) =
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -1190,7 +1190,6 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_inductives}
     "print (co)inductive definitions and monotonicity rules"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (print_inductives b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of)));
 
 end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -154,7 +154,6 @@
 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
 
 fun try0_trans quad =
-  Toplevel.unknown_proof o
   Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
 
 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
diff -r 0a064330a885 -r f5c4b49c8c9a src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Provers/classical.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -980,6 +980,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of)));
 
 end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/General/graph_display.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -11,6 +11,7 @@
   val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
   type entry = (string * node) * string list
   val display_graph: entry list -> unit
+  val display_graph_old: entry list -> unit
 end;
 
 structure Graph_Display: GRAPH_DISPLAY =
@@ -30,7 +31,9 @@
 type entry = (string * node) * string list;
 
 
-(* encode graph *)
+(* display graph *)
+
+local
 
 fun encode_node (Node {name, content, ...}) =
   (name, content) |>
@@ -40,9 +43,22 @@
 val encode_graph =
   let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
 
+in
+
+fun display_graph entries =
+  let
+    val ((bg1, bg2), en) =
+      YXML.output_markup_elem
+        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+  in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
+
+end;
+
 
 (* support for old browser *)
 
+local
+
 structure Graph =
   Graph(type key = string * string val ord = prod_ord string_ord string_ord);
 
@@ -71,23 +87,15 @@
     path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
   #> cat_lines;
 
+in
 
-(* display graph *)
-
-fun display_graph entries =
+fun display_graph_old entries =
   let
     val ((bg1, bg2), en) =
       YXML.output_markup_elem
-        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
-    val _ =
-      writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
-
-    (*old browser*)
-    val ((bg1, bg2), en) =
-      YXML.output_markup_elem
         (Active.make_markup Markup.browserN {implicit = false, properties = []});
-    val _ =
-      writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
-  in () end;
+  in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
 
 end;
+
+end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/calculation.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -230,6 +230,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
 
 end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -35,8 +35,6 @@
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
   val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
-  val thy_deps: Toplevel.transition -> Toplevel.transition
-  val locale_deps: Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (Facts.ref * Token.src list) list
     -> Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (Facts.ref * Token.src list) list
@@ -241,10 +239,7 @@
   in ML_Context.eval_source_in opt_ctxt flags source end);
 
 val diag_state = Diag_State.get;
-
-fun diag_goal ctxt =
-  Proof.goal (Toplevel.proof_of (diag_state ctxt))
-    handle Toplevel.UNDEF => error "No goal present";
+val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
 
 val _ = Theory.setup
   (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
@@ -268,26 +263,6 @@
     in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
 
 
-(* display dependencies *)
-
-val thy_deps =
-  Toplevel.unknown_theory o
-  Toplevel.keep (fn st =>
-    let
-      val thy = Toplevel.theory_of st;
-      val parent_session = Session.get_name ();
-      val parent_loaded = is_some o Thy_Info.lookup_theory;
-    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
-
-val locale_deps =
-  Toplevel.unknown_theory o
-  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
-    Locale.pretty_locale_deps thy
-    |> map (fn {name, parents, body} =>
-      ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
-    |> Graph_Display.display_graph));
-
-
 (* print theorems, terms, types etc. *)
 
 local
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -350,8 +350,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_bundles}
     "print bundles of declarations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
 
 
 (* local theories *)
@@ -693,8 +692,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_options} "print configuration options"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_context}
@@ -704,125 +702,116 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_theory}
     "print logical theory contents"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_syntax}
     "print inner syntax of context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_defn_rules}
     "print definitional rewrite rules of context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_abbrevs}
     "print constant abbreviations of context"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_theorems}
     "print theorems of local theory or proof context"
     (Parse.opt_bang >> (fn b =>
-      Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_locales}
     "print locales of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_classes}
     "print classes of this theory"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Class.print_classes o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_locale}
     "print locale of this theory"
     (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
-      Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_interps}
     "print interpretations of locale for this theory or proof context"
     (Parse.position Parse.xname >> (fn name =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_dependencies}
     "print dependencies of locale expression"
     (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_attributes}
     "print attributes of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
-      Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_simpset}
     "print context of Simplifier"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
-      Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_antiquotations}
     "print document antiquotations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_ML_antiquotations}
     "print ML antiquotations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
-    (Scan.succeed Isar_Cmd.thy_deps);
-
-val _ =
   Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
-    (Scan.succeed Isar_Cmd.locale_deps);
+    (Scan.succeed
+      (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
+        Locale.pretty_locale_deps thy
+        |> map (fn {name, parents, body} =>
+          ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+        |> Graph_Display.display_graph))));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_term_bindings}
     "print term bindings of proof context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep
+    (Scan.succeed
+      (Toplevel.keep
         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+    (Scan.succeed
+      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_statement}
@@ -856,8 +845,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_state}
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -19,6 +19,7 @@
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_keyword -> string ->
     (local_theory -> Proof.state) parser -> unit
+  val bootstrap: bool Config.T
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
@@ -160,6 +161,9 @@
 
 (* parse commands *)
 
+val bootstrap =
+  Config.bool (Config.declare ("Outer_Syntax.bootstrap", @{here}) (K (Config.Bool true)));
+
 local
 
 val before_command =
@@ -177,7 +181,14 @@
       | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
           before_command :|-- (fn limited =>
             Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
-      | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
+      | NONE =>
+          Scan.fail_with (fn _ => fn _ =>
+            let
+              val msg =
+                if Config.get_global thy bootstrap
+                then "missing theory context for command "
+                else "undefined command ";
+            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
     end);
 
 val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -338,7 +338,7 @@
   fun find i state =
     (case try current_goal state of
       SOME (ctxt, goal) => (ctxt, (i, goal))
-    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
+    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal"));
 in val find_goal = find 0 end;
 
 fun get_goal state =
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -72,9 +72,6 @@
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val exec_id: Document_ID.exec -> transition -> transition
-  val unknown_theory: transition -> transition
-  val unknown_proof: transition -> transition
-  val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
   val get_timing: transition -> Time.time option
@@ -164,12 +161,12 @@
 val context_of = node_case Context.proof_of Proof.context_of;
 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
 val theory_of = node_case Context.theory_of Proof.theory_of;
-val proof_of = node_case (fn _ => raise UNDEF) I;
+val proof_of = node_case (fn _ => error "No proof state") I;
 
 fun proof_position_of state =
   (case node_of state of
     Proof (prf, _) => Proof_Node.position prf
-  | _ => raise UNDEF);
+  | _ => ~1);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
@@ -356,10 +353,6 @@
 fun malformed pos msg =
   empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
 
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_proof = imperative (fn () => warning "Unknown proof context");
-val unknown_context = imperative (fn () => warning "Unknown context");
-
 
 (* theory transitions *)
 
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -53,15 +53,13 @@
 
   ML_Antiquotation.value @{binding theory}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      (Context_Position.report ctxt pos
-        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+      (Theory.check ctxt (name, pos);
        "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
     || Scan.succeed "Proof_Context.theory_of ML_context") #>
 
   ML_Antiquotation.value @{binding theory_context}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      (Context_Position.report ctxt pos
-        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+      (Theory.check ctxt (name, pos);
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>
 
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -109,11 +109,10 @@
       | NONE => toks)
   | _ => toks);
 
-val bootstrap_thy = ML_Context.the_global_context ();
-
 in
 
-fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
+fun read_thy st = Toplevel.theory_of st
+  handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy;
 
 fun read keywords thy master_dir init blobs_info span =
   let
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 16 20:54:01 2015 +0200
@@ -98,6 +98,7 @@
 ML_file "Tools/rail.ML"
 ML_file "Tools/rule_insts.ML"
 ML_file "Tools/thm_deps.ML"
+ML_file "Tools/thy_deps.ML"
 ML_file "Tools/class_deps.ML"
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -540,11 +540,7 @@
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
-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.here pos)
-  | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
+fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
 
 
 (* default output *)
@@ -614,16 +610,12 @@
 
 local
 
-fun proof_state state =
-  (case try (Proof.goal o Toplevel.proof_of) state of
-    SOME {goal, ...} => goal
-  | _ => error "No proof state");
-
 fun goal_state name main = antiquotation name (Scan.succeed ())
   (fn {state, context = ctxt, ...} => fn () =>
     output ctxt
       [Goal_Display.pretty_goal
-        (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
+        (Config.put Goal_Display.show_main_goal main ctxt)
+        (#goal (Proof.goal (Toplevel.proof_of state)))]);
 
 in
 
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -6,49 +6,44 @@
 
 signature CLASS_DEPS =
 sig
-  val class_deps: Proof.context -> sort list option -> sort list option -> unit
-  val class_deps_cmd: Proof.context -> string list option -> string list option -> unit
+  val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list
+  val class_deps_cmd: Proof.context -> string list option * string list option -> unit
 end;
 
 structure Class_Deps: CLASS_DEPS =
 struct
 
-fun gen_class_deps prep_sort ctxt raw_subs raw_supers =
+fun gen_class_deps prep_sort ctxt bounds =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val some_subs = (Option.map o map) (prep_sort ctxt) raw_subs;
-    val some_supers = (Option.map o map) (prep_sort ctxt) raw_supers;
-    val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
-    val sort_le = curry (Sorts.sort_le original_algebra);
-    val le_sub = case some_subs of
-      SOME subs => (fn class => exists (sort_le [class]) subs)
-    | NONE => K true;
-    val super_le = case some_supers of
-      SOME supers => (fn class => exists (fn super => sort_le super [class]) supers)
-    | NONE => K true
-    val (_, algebra) =
-      Sorts.subalgebra (Context.pretty ctxt)
-        (le_sub andf super_le) (K NONE) original_algebra;
+    val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds;
+    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+    val rel = Sorts.sort_le algebra;
+    val pred =
+      (case upper of
+        SOME bs => (fn c => exists (fn b => rel ([c], b)) bs)
+      | NONE => K true) andf
+      (case lower of
+        SOME bs => (fn c => exists (fn b => rel (b, [c])) bs)
+      | NONE => K true);
     fun node c =
       Graph_Display.content_node (Name_Space.extern ctxt space c)
-        (Class.pretty_specification thy c);
+        (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
   in
-    Sorts.classes_of algebra
-    |> Graph.dest
+    Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
+    |> #2 |> Sorts.classes_of |> Graph.dest
     |> map (fn ((c, _), ds) => ((c, node c), ds))
-    |> Graph_Display.display_graph
   end;
 
 val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
-val class_deps_cmd = gen_class_deps Syntax.read_sort;
+val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
 
-val parse_sort_list = (Parse.sort >> single)
-  || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
+val class_bounds =
+  Parse.sort >> single ||
+  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
 
 val _ =
   Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
-    ((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
-      (Toplevel.unknown_theory o
-       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
+    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
+      Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args)));
 
 end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -44,14 +44,14 @@
         else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
   in
     Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
-    |> Graph_Display.display_graph
+    |> Graph_Display.display_graph_old
   end;
 
 val _ =
   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
     (Parse.xthms1 >> (fn args =>
-      Toplevel.unknown_theory o Toplevel.keep (fn state =>
-        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+      Toplevel.keep (fn st =>
+        thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
 
 
 (* unused_thms *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/Tools/thy_deps.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/thy_deps.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -0,0 +1,54 @@
+(*  Title:      Pure/Tools/thy_deps.ML
+    Author:     Makarius
+
+Visualization of theory dependencies.
+*)
+
+signature THY_DEPS =
+sig
+  val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
+  val thy_deps_cmd: Proof.context ->
+    (string * Position.T) list option * (string * Position.T) list option -> unit
+end;
+
+structure Thy_Deps: THY_DEPS =
+struct
+
+fun gen_thy_deps _ ctxt (NONE, NONE) =
+      let
+        val parent_session = Session.get_name ();
+        val parent_loaded = is_some o Thy_Info.lookup_theory;
+      in Present.session_graph parent_session parent_loaded (Proof_Context.theory_of ctxt) end
+  | gen_thy_deps prep_thy ctxt bounds =
+      let
+        val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
+        val rel = Theory.subthy o swap;
+        val pred =
+          (case upper of
+            SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
+          | NONE => K true) andf
+          (case lower of
+            SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
+          | NONE => K true);
+        fun node thy =
+          ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
+            map Context.theory_name (filter pred (Theory.parents_of thy)));
+      in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
+
+val thy_deps =
+  gen_thy_deps (fn ctxt => fn thy =>
+    let val thy0 = Proof_Context.theory_of ctxt
+    in if Theory.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 theory_bounds =
+  Parse.position Parse.theory_xname >> single ||
+  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
+
+val _ =
+  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
+    (Scan.option theory_bounds -- Scan.option theory_bounds >>
+      (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.context_of st) args)));
+
+end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/pure_syn.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -1,10 +1,16 @@
 (*  Title:      Pure/pure_syn.ML
     Author:     Makarius
 
-Outer syntax for bootstrapping Isabelle/Pure.
+Outer syntax for bootstrapping: commands that are accessible outside a
+regular theory context.
 *)
 
-structure Pure_Syn: sig end =
+signature PURE_SYN =
+sig
+  val bootstrap_thy: theory
+end;
+
+structure Pure_Syn: PURE_SYN =
 struct
 
 val _ =
@@ -44,5 +50,9 @@
     (Thy_Header.args >>
       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
+
+val bootstrap_thy = ML_Context.the_global_context ();
+
+val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
+
 end;
-
diff -r 0a064330a885 -r f5c4b49c8c9a src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/theory.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -16,6 +16,7 @@
   val setup: (theory -> theory) -> unit
   val local_setup: (Proof.context -> Proof.context) -> unit
   val get_markup: theory -> Markup.T
+  val check: 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
@@ -128,6 +129,25 @@
   let val {pos, id, ...} = rep_theory thy
   in theory_markup false (Context.theory_name thy) id pos end;
 
+fun check ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val thy' =
+      Context.get_theory thy name
+        handle ERROR msg =>
+          let
+            val completion =
+              Completion.make (name, pos)
+                (fn completed =>
+                  map Context.theory_name (ancestors_of thy)
+                  |> filter completed
+                  |> 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;
+    val _ = Context_Position.report ctxt pos (get_markup thy');
+  in thy' end;
+
 
 (* basic operations *)
 
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -589,6 +589,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of)));
 
 end; (*struct*)
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -946,7 +946,7 @@
     |> join_strong_conn
     |> Graph.dest
     |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
-    |> Graph_Display.display_graph
+    |> Graph_Display.display_graph_old
   end;
 
 local
@@ -960,14 +960,12 @@
   Outer_Syntax.command @{command_keyword code_thms}
     "print system of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_context o
-      Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
+      Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
 
 val _ =
   Outer_Syntax.command @{command_keyword code_deps}
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
 
 end;
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/induct.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -257,8 +257,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_induct_rules}
     "print induction and cases rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
 (* access rules *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -533,8 +533,8 @@
 val _ =
   Outer_Syntax.command @{command_keyword quickcheck}
     "try to find counterexample for subgoal"
-    (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
-      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
+    (parse_args -- Scan.optional Parse.nat 1 >>
+      (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
 
 
 (* automatic testing *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/solve_direct.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -94,8 +94,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword solve_direct}
     "try to solve conjectures directly with existing theorems"
-    (Scan.succeed (Toplevel.unknown_proof o
-      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/Tools/try.ML
--- a/src/Tools/try.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Tools/try.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -77,7 +77,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword try}
     "try a combination of automatic proving and disproving tools"
-    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
 
 (* automatic try (TTY) *)
diff -r 0a064330a885 -r f5c4b49c8c9a src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/ZF/Tools/typechk.ML	Thu Apr 16 20:54:01 2015 +0200
@@ -127,7 +127,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_tcset o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of)));
 
 end;