--- a/ProgTutorial/antiquote_setup.ML	Mon Aug 03 16:47:01 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Aug 04 16:18:39 2009 +0200
@@ -106,22 +106,22 @@
 
 (* replaces the official subgoal antiquotation with one *)
 (* that is closer to the actual output                  *)
+fun proof_state state =
+    (case try Toplevel.proof_of state of
+      SOME prf => prf
+    | _ => error "No proof state")
+
 fun output_goals  {state = node, ...}  _ = 
 let
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
-  fun proof_state state =
-    (case try Toplevel.proof_of state of
-      SOME prf => prf
-    | _ => error "No proof state")
-
   val state = proof_state node;
   val goals = Pretty.chunks (Proof.pretty_goals false state);
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
-  val (As, B) = Logic.strip_horn prop;
+  val (As, _) = Logic.strip_horn prop;
   val output  = (case (length As) of
                       0 => [goals] 
                     | n => [Pretty.str (subgoals n), goals])  
@@ -129,6 +129,20 @@
   ThyOutput.output output
 end
 
+fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
+let
+  val state = proof_state node;
+  val goals = (Proof.get_goal state |> snd |> snd)
+
+  val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
+  val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
+  val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
+in 
+  ThyOutput.output output
+end
+
+
 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
- 
+val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
+
 end;