diff -r a99aa67455f3 -r 0a5c95f4d70c CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Thu Feb 05 22:39:37 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Thu Feb 05 22:40:22 2009 +0000
@@ -60,7 +60,7 @@
 (* to be closer to the actual output *)
 fun output_goals main_goal src node = 
 let 
-  fun subgoals 0 = "No subgoals!"
+  fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):";
  
@@ -69,12 +69,17 @@
           SOME (SOME prf) => ProofNode.current prf
         | _ => error "No proof state");
 
-  val state = proof_state node
+  val state = proof_state node;
   val goals = Proof.pretty_goals main_goal state;
-  val msg  = Pretty.str (subgoals (length goals))  
+
+  val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
+  val (As, B) = Logic.strip_horn prop;
+  val output  = (case (length As) of
+                      0 => goals 
+                    | n => (Pretty.str (subgoals n))::goals)  
 in 
   ThyOutput.args (Scan.succeed ()) 
-   (Chunks.output (fn _ => fn _ => Pretty.chunks (msg::goals))) src node
+   (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node
 end