# HG changeset patch
# User wenzelm
# Date 1662459957 -7200
# Node ID 8e1b2e1a29b722efccc68c4120b6ce43d5d46c94
# Parent  cf13b2147c48adf3607e8a22896216754d06c4d9
proper antiquotations;

diff -r cf13b2147c48 -r 8e1b2e1a29b7 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 06 11:55:24 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 06 12:25:57 2022 +0200
@@ -248,7 +248,7 @@
 
 (* goal instantiation *)
 
-val show_goal_inst = Attrib.setup_option_bool ("show_goal_inst", \<^here>);
+val show_goal_inst = Attrib.setup_option_bool (\<^system_option>\<open>show_goal_inst\<close>, \<^here>);
 
 fun pretty_goal_inst ctxt propss goal =
   let