diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,392 +1,390 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = "" (standard "true")
   -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
 option document_output : string = "" (standard "output")
   -- "document output directory"
 option document_echo : bool = false
   -- "inform about document file names during session presentation"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 option document_bibliography : bool = false
   -- "explicitly enable use of bibtex (default: according to presence of root.bib)"
 option document_build : string = "lualatex" (standard "build")
   -- "document build engine (e.g. build, lualatex, pdflatex)"
 option document_logo : string = ""
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
 option document_heading_prefix : string = "isamarkup" (standard)
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
 option document_comment_latex : bool = false
   -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
 option thy_output_cartouche : bool = false
   -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 option thy_output_source_cartouche : bool = false
   -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
 
 section "Prover Output"
 
 option show_types : bool = false
   -- "show type constraints when printing terms"
 option show_sorts : bool = false
   -- "show sort constraints when printing types"
 option show_brackets : bool = false
   -- "show extra brackets when printing terms/types"
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
-option show_goal_inst : bool = true
-  -- "show goal instantiation (for schematic goals)"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
 option show_states : bool = false
   -- "show toplevel states even if outside of interactive mode"
 
 
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
   -- "show base names only"
 option names_unique : bool = true
   -- "show partially qualified names, as required for unique name resolution"
 
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
 
 section "Parallel Processing and Timing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
 public option parallel_limit : int = 0
   -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"
 
 public option timeout_scale : real = 1.0
   -- "scale factor for timeout in Isabelle/ML and session build"
 
 
 section "Detail of Proof Checking"
 
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 option strict_facts : bool = false
   -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
 option timeout_build : bool = true
   -- "observe timeout for session build"
 
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = "" (standard "time")
   -- "ML profiling (possible values: time, time_thread, allocations)"
 
 option system_log : string = "" (standard "-")
   -- "output for system messages (log file or \"-\" for console progress)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
 
 section "ML System"
 
 option ML_print_depth : int = 20
   -- "ML print depth for toplevel pretty-printing"
 
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
 public option ML_exception_debugger : bool = false
   -- "ML debugger exception trace for toplevel command execution"
 
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
 
 section "PIDE Build"
 
 option pide_reports : bool = true
   -- "report PIDE markup"
 
 option build_pide_reports : bool = true
   -- "report PIDE markup in batch build"
 
 
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
 public option editor_input_delay : real = 0.2
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
   -- "delay for machine-generated input that may outperform user edits"
 
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
 public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 option editor_prune_size : int = 0
   -- "retained size of pruned history (delete old versions)"
 
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
 public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
 public option editor_presentation : bool = false
   -- "dynamic presentation while editing"
 
 
 section "Headless Session"
 
 option headless_consolidate_delay : real = 15
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 option headless_prune_delay : real = 60
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
 option headless_check_limit : int = 0
   -- "maximum number of theory status checks (0 = unlimited)"
 
 option headless_nodes_status_delay : real = -1
   -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
 
 option headless_watchdog_timeout : real = 600
   -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
 
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
 option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
 
 public option find_theorems_limit : int = 40
   -- "limit of displayed results"
 
 public option find_theorems_tactic_limit : int = 5
   -- "limit of tactic search for 'solves' criterion"
 
 
 section "Completion"
 
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
 public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
 section "Spell Checker"
 
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
 public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"
 
 option ssh_config_dir : string = "$HOME/.ssh"
   -- "SSH configuration directory"
 
 option ssh_config_file : string = "$HOME/.ssh/config"
   -- "main SSH configuration file"
 
 option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
   -- "possible SSH identity files (separated by colons)"
 
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
 option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive"
 
 
 section "Phabricator"
 
 option phabricator_version_arcanist : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a"
   -- "repository version for arcanist"
 
 option phabricator_version_phabricator : string = "193798385bd3a7f72dca255e44f8112f4f8fc155"
   -- "repository version for phabricator"
 
 
 section "Theory Export"
 
 option export_theory : bool = false
   -- "export theory content to Isabelle/Scala"
 
 option export_standard_proofs : bool = false
   -- "export standardized proof terms to Isabelle/Scala (not scalable)"
 
 option export_proofs : bool = false
   -- "export proof terms to Isabelle/Scala"
 
 option prune_proofs : bool = false
   -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
 
 option update_inner_syntax_cartouches : bool = false
   -- "update inner syntax (types, terms, etc.) to use cartouches"
 
 option update_mixfix_cartouches : bool = false
   -- "update mixfix templates to use cartouches instead of double quotes"
 
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
 
 section "Build Database"
 
 option build_database_server : bool = false
 option build_database_user : string = ""
 option build_database_password : string = ""
 option build_database_name : string = ""
 option build_database_host : string = ""
 option build_database_port : int = 0
 option build_database_ssh_host : string = ""
 option build_database_ssh_user : string = ""
 option build_database_ssh_port : int = 0
 
 
 section "Build Log Database"
 
 option build_log_database_user : string = ""
 option build_log_database_password : string = ""
 option build_log_database_name : string = ""
 option build_log_database_host : string = ""
 option build_log_database_port : int = 0
 option build_log_ssh_host : string = ""
 option build_log_ssh_user : string = ""
 option build_log_ssh_port : int = 0
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
 
 
 section "Isabelle/Scala/ML system channel"
 
 option system_channel_address : string = ""
 option system_channel_password : string = ""
 
 
 section "Bash process execution server"
 
 option bash_process_debugging : bool = false
 option bash_process_address : string = ""
 option bash_process_password : string = ""
diff --git a/src/Pure/Isar/proof_display.ML b/src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML
+++ b/src/Pure/Isar/proof_display.ML
@@ -1,399 +1,394 @@
 (*  Title:      Pure/Isar/proof_display.ML
     Author:     Makarius
 
 Printing of theorems, goals, results etc.
 *)
 
 signature PROOF_DISPLAY =
 sig
   val pp_context: Proof.context -> Pretty.T
   val pp_thm: (unit -> theory) -> thm -> Pretty.T
   val pp_typ: (unit -> theory) -> typ -> Pretty.T
   val pp_term: (unit -> theory) -> term -> Pretty.T
   val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
   val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
   val pretty_theory: bool -> Proof.context -> Pretty.T
   val pretty_definitions: bool -> Proof.context -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
   val pretty_theorems: bool -> Proof.context -> Pretty.T list
   val string_of_rule: Proof.context -> string -> thm -> string
   val pretty_goal_header: thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
   val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
-  val show_goal_inst: bool Config.T
   val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val show_results: bool Config.T
   val print_results: bool -> Position.T -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
 end
 
 structure Proof_Display: PROOF_DISPLAY =
 struct
 
 (** toplevel pretty printing **)
 
 fun pp_context ctxt =
  (if Config.get ctxt Proof_Context.debug then
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
 fun default_context mk_thy =
   (case Context.get_generic_context () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
       (case try Syntax.init_pretty_global thy of
         SOME ctxt => ctxt
       | NONE => Syntax.init_pretty_global (mk_thy ()))
   | NONE => Syntax.init_pretty_global (mk_thy ()));
 
 fun pp_thm mk_thy th =
   Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
 
 fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
 fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
 
 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
 fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
 
 
 
 (** theory content **)
 
 fun pretty_theory verbose ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun prt_cls c = Syntax.pretty_sort ctxt [c];
     fun prt_sort S = Syntax.pretty_sort ctxt S;
     fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
           (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
 
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
     fun pretty_type syn (t, Type.LogicalType n) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
       | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
       | pretty_type syn (t, Type.Nonterminal) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));
 
     val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
 
     fun pretty_abbrev (c, (ty, t)) = Pretty.block
       (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
 
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
     val {const_space, constants, constraints} = Consts.dest consts;
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val type_space = Type.type_space tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
       Name_Space.extern_entries verbose ctxt class_space
         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
       |> map (apfst #1);
     val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
     val arties =
       Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities)
       |> map (apfst #1);
 
     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
   in
     Pretty.chunks
      [Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
       Pretty.big_list "type arities:" (pretty_arities arties),
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.block
         (Pretty.breaks (Pretty.str "oracles:" ::
           map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
   end;
 
 
 (* theorems *)
 
 fun pretty_theorems_diff verbose prev_thys ctxt =
   let
     val pretty_fact = Proof_Context.pretty_fact ctxt;
     val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
     val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
   in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
 
 fun pretty_theorems verbose ctxt =
   pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
 
 
 (* definitions *)
 
 fun pretty_definitions verbose ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val context = Proof_Context.defs_context ctxt;
 
     val const_space = Proof_Context.const_space ctxt;
     val type_space = Proof_Context.type_space ctxt;
     val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
 
     fun extern_item (kind, name) =
       let val xname = Name_Space.extern ctxt (item_space kind) name
       in (xname, (kind, name)) end;
 
     fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
       (case Defs.item_kind_ord (kind1, kind2) of
         EQUAL => string_ord (xname1, xname2)
       | ord => ord);
 
     fun sort_items f = sort (extern_item_ord o apply2 f);
 
     fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
       ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
         Pretty.commas (map pretty_entry (sort_items fst rhs)));
 
     fun pretty_restrict (entry, name) =
       Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
 
     val (reds1, reds2) =
       filter_out (prune_item o #1 o #1) reducts
       |> map (fn (lhs, rhs) =>
         (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
       |> sort_items (#1 o #1)
       |> filter_out (null o #2)
       |> List.partition (Defs.plain_args o #2 o #1);
 
     val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
   in
     Pretty.big_list "definitions:"
       (map (Pretty.text_fold o single)
         [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
          Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
          Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
   end;
 
 
 
 (** proof items **)
 
 (* refinement rule *)
 
 fun pretty_rule ctxt s thm =
   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
     Pretty.fbrk, Thm.pretty_thm ctxt thm];
 
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
 
 (* goals *)
 
 local
 
 fun subgoals 0 = []
   | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
 
 in
 
 fun pretty_goal_header goal =
   Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
 
 end;
 
 fun string_of_goal ctxt goal =
   Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
 
 
 (* goal facts *)
 
 fun pretty_goal_facts _ _ NONE = []
   | pretty_goal_facts ctxt s (SOME ths) =
       (single o Pretty.block o Pretty.fbreaks)
         [if s = "" then Pretty.str "this:"
          else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
          Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* goal instantiation *)
 
-val show_goal_inst = Attrib.setup_option_bool (\<^system_option>\<open>show_goal_inst\<close>, \<^here>);
-
 fun pretty_goal_inst ctxt propss goal =
   let
     val title = "goal instantiation:";
 
     fun prt_inst env =
       if Envir.is_empty env then []
       else
         let
           val Envir.Envir {tyenv, tenv, ...} = env;
 
           val prt_type = Syntax.pretty_typ ctxt;
           val prt_term = Syntax.pretty_term ctxt;
 
           fun instT v =
             let
               val T = TVar v;
               val T' = Envir.subst_type tyenv T;
             in if T = T' then NONE else SOME (prt_type T, prt_type T') end;
 
           fun inst v =
             let
               val t = Var v;
               val t' = Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
             in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
 
           fun inst_pair (x, y) = Pretty.item [x, Pretty.str " \<leadsto>", Pretty.brk 1, y];
 
           val prts =
             ((fold o fold) Term.add_tvars propss [] |> sort Term_Ord.tvar_ord |> map_filter instT) @
             ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
         in if null prts then [] else [Pretty.big_list title (map inst_pair prts)] end;
 
     exception LOST_STRUCTURE;
     fun goal_matcher () =
       let
         val concl =
           Logic.unprotect (Thm.concl_of goal)
             handle TERM _ => raise LOST_STRUCTURE;
         val goal_propss = filter_out null propss;
         val results =
           Logic.dest_conjunction_balanced (length goal_propss) concl
           |> map2 Logic.dest_conjunction_balanced (map length goal_propss)
             handle TERM _ => raise LOST_STRUCTURE;
       in
         Unify.matcher (Context.Proof ctxt)
           (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (flat results)
       end;
 
     fun failure msg = (warning (title ^ " " ^ msg); []);
   in
-    if Config.get ctxt show_goal_inst then
-      (case goal_matcher () of
-        SOME env => prt_inst env
-      | NONE => failure "match failed")
-      handle LOST_STRUCTURE => failure "lost goal structure"
-    else []
+    (case goal_matcher () of
+      SOME env => prt_inst env
+    | NONE => failure "match failed")
+    handle LOST_STRUCTURE => failure "lost goal structure"
   end;
 
 
 (* method_error *)
 
 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   let
     val pr_header =
       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
       "proof method" ^ Position.here pos ^ ":\n";
     val pr_facts =
       if null facts then ""
       else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
     val pr_goal = string_of_goal ctxt goal;
   in pr_header ^ pr_facts ^ pr_goal end);
 
 
 (* results *)
 
 fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
 
 val interactive =
   Config.declare_bool ("interactive", \<^here>) (K false);
 
 val show_results =
   Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
     (fn context =>
       Config.get_generic context interactive orelse
       Options.default_bool \<^system_option>\<open>show_states\<close>);
 
 fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
 
 local
 
 fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
   | pretty_fact_name pos (kind, name) =
       Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
   flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
     map (single o Proof_Context.pretty_fact ctxt);
 
 in
 
 fun print_results int pos ctxt ((kind, name), facts) =
   if kind = "" orelse no_print int ctxt then ()
   else if name = "" then
     (Output.state o Pretty.string_of)
       (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
         pretty_facts ctxt facts))
   else
     (Output.state o Pretty.string_of)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])
       | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
 end;
 
 
 (* consts *)
 
 local
 
 fun pretty_var ctxt (x, T) =
   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
     Pretty.quote (Syntax.pretty_typ ctxt T)];
 
 fun pretty_vars pos ctxt kind vs =
   Pretty.block
     (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
 
 val fixes = (Markup.keyword2, "fixes");
 val consts = (Markup.keyword1, "consts");
 
 fun pretty_consts pos ctxt pred cs =
   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
     [] => pretty_vars pos ctxt consts cs
   | ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]);
 
 in
 
 fun print_consts int pos ctxt pred cs =
   if null cs orelse no_print int ctxt then ()
   else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
 
 end;
 
 end;