# HG changeset patch
# User paulson
# Date 862827320 -7200
# Node ID e8a92f49729534de5fcf275dc2cd80216cdcc8d1
# Parent  2b0f9ff0601867abbf80d7946c8baabcfb20549c
Again "norm" DOES NOT normalize bodies of abstractions

Showterm (used for tracing) now follows variable instantiations (in order
to make up for the "norm" change)

diff -r 2b0f9ff06018 -r e8a92f497295 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri May 02 18:19:25 1997 +0200
+++ b/src/Provers/blast.ML	Mon May 05 12:15:20 1997 +0200
@@ -300,15 +300,14 @@
   in  subst (t,0)  end;
 
 
-(*Normalize, INCLUDING bodies of abstractions--this might be slow?*)
+(*Normalize...but not the bodies of ABSTRACTIONS*)
 fun norm t = case t of
     Skolem (a,args)      => Skolem(a, vars_in_vars args)
   | (Var (ref None))     => t
   | (Var (ref (Some u))) => norm u
   | (f $ u) => (case norm f of
-		    Abs(_,body) => norm (subst_bound (u, body))
-		  | nf => nf $ norm u)
-  | Abs (a,body) => Abs (a, norm body)
+                    Abs(_,body) => norm (subst_bound (u, body))
+                  | nf => nf $ norm u)
   | _ => t;
 
 
@@ -490,8 +489,7 @@
 end;
 
 
-(*** Conversion of Introduction Rules (needed for efficiency in 
-               proof reconstruction) ***)
+(*** Conversion of Introduction Rules ***)
 
 fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
 
@@ -573,7 +571,8 @@
   | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   | showTerm d (Free a)      = Term.Free  (a,dummyT)
   | showTerm d (Bound i)     = Term.Bound i
-  | showTerm d (Var _)       = dummyVar2
+  | showTerm d (Var(ref(Some u))) = showTerm d u
+  | showTerm d (Var(ref None))    = dummyVar2
   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
 			       else Term.Abs(a, dummyT, showTerm (d-1) t)
   | showTerm d (f $ u)       = if d=0 then dummyVar
@@ -1008,6 +1007,8 @@
 		       else 
 			 traceNew prems;  traceVars ntrl;
 			 prv(tac dup :: tacs, 
+			       (*FIXME: if recur then the tactic should not
+				 call rotate_tac: new formulae should be last*)
 			     brs0::trs, 
 			     (ntrl, length brs0, PRV) :: choices, 
 			     newBr (vars', recur, dup, lim') prems)