# HG changeset patch
# User paulson
# Date 1139918580 -3600
# Node ID 3be721728a6cfb428ab65ebcd90ea2996176b829
# Parent  73782d21e855b9010b7ce6d6efdf9a2518e317fa
fixed tracing

diff -r 73782d21e855 -r 3be721728a6c src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Feb 13 17:02:54 2006 +0100
+++ b/src/Provers/blast.ML	Tue Feb 14 13:03:00 2006 +0100
@@ -604,8 +604,24 @@
 
 fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
 
+(*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
+  Ex(P) is duplicated as the assumption ~Ex(P). *)
+fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
+  | negOfGoal G = G;
+
+fun negOfGoal2 (G,md) = (negOfGoal G, md);
+
+(*Converts all Goals to Nots in the safe parts of a branch.  They could
+  have been moved there from the literals list after substitution (equalSubst).
+  There can be at most one--this function could be made more efficient.*)
+fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
+
+(*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
+fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
+                      rotate_tac ~1 i;
+
 fun traceTerm sign t =
-  let val t' = norm t
+  let val t' = norm (negOfGoal t)
       val stm = string_of sign 8 t'
   in
       case topType sign t' of
@@ -792,22 +808,6 @@
 fun joinMd md [] = []
   | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
 
-(*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
-  Ex(P) is duplicated as the assumption ~Ex(P). *)
-fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
-  | negOfGoal G = G;
-
-fun negOfGoal2 (G,md) = (negOfGoal G, md);
-
-(*Converts all Goals to Nots in the safe parts of a branch.  They could
-  have been moved there from the literals list after substitution (equalSubst).
-  There can be at most one--this function could be made more efficient.*)
-fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
-
-(*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
-fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
-                      rotate_tac ~1 i;
-
 
 (** Backtracking and Pruning **)