--- a/ProgTutorial/antiquote_setup.ML	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Wed May 22 12:38:51 2019 +0200
@@ -220,26 +220,6 @@
     SOME {goal, ...} => goal
   | _ => error "No proof state");
 
-
-fun output_goals ctxt _ = 
-let
-  fun subgoals 0 = ""
-    | subgoals 1 = "goal (1 subgoal):"
-    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
-
-  val state = proof_state (Toplevel.presentation_state ctxt)
-  val goals = Goal_Display.pretty_goal ctxt state
-
-  val prop = Thm.prop_of state;
-  val (As, _) = Logic.strip_horn prop;
-  val out  = (case (length As) of
-                      0 => goals 
-                    | n => Pretty.big_list (subgoals n) [goals])  (* FIXME: improve printing? *)
-in 
-  output ctxt [Pretty.string_of out]
-end
-
-
 fun output_raw_goal_state  ctxt  _ = 
   let
     val goals = proof_state (Toplevel.presentation_state ctxt)
@@ -248,14 +228,11 @@
     output ctxt [out]
   end
 
-val subgoals_setup = 
-  Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals
 val raw_goal_state_setup = 
   Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
 
 val setup =
   ml_setup #>
   ml_file_setup #>
-  subgoals_setup #>
   raw_goal_state_setup
 end;