# HG changeset patch
# User wenzelm
# Date 1662725009 -7200
# Node ID 7cac5565e79bcae21f6290a15a2a3e3de75b42fc
# Parent  4dec713d3bc9f6f9cbb24dca97b25bbe1bf68750
discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);

diff -r 4dec713d3bc9 -r 7cac5565e79b etc/options
--- a/etc/options	Thu Sep 08 22:59:21 2022 +0200
+++ b/etc/options	Fri Sep 09 14:03:29 2022 +0200
@@ -59,8 +59,6 @@
 
 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
diff -r 4dec713d3bc9 -r 7cac5565e79b src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Sep 08 22:59:21 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 09 14:03:29 2022 +0200
@@ -20,7 +20,6 @@
   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
@@ -248,8 +247,6 @@
 
 (* 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:";
@@ -300,12 +297,10 @@
 
     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;