# HG changeset patch
# User wenzelm
# Date 1662670761 -7200
# Node ID 4dec713d3bc9f6f9cbb24dca97b25bbe1bf68750
# Parent  ce66ff654e599a6e2cb9d56ec6a5933fa9af8570
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;

diff -r ce66ff654e59 -r 4dec713d3bc9 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Thu Sep 08 22:35:50 2022 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Thu Sep 08 22:59:21 2022 +0200
@@ -10,8 +10,6 @@
 
 ML_file \<open>prolog.ML\<close>
 
-declare [[show_main_goal]]
-
 method_setup ptac =
   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
   "basic Lambda Prolog interpreter"