diff -r 69def2a31fad -r ea834e8fac1b src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Apr 15 10:19:14 1997 +0200
+++ b/src/Provers/blast.ML	Tue Apr 15 10:22:50 1997 +0200
@@ -5,6 +5,8 @@
 
 Generic tableau prover with proof reconstruction
 
+  Why does Abs take a string argument?
+
   SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
   Needs explicit instantiation of assumptions?
 
@@ -20,6 +22,15 @@
   * its proof strategy is more general but can actually be slower
 
 Known problems:
+  With overloading:
+    1.  Overloading can't follow all chains of type dependencies.  Cannot
+        prove "In1 x ~: Part A In0" because PartE introducees the polymorphic
+	equality In1 x = In0 y, when the corresponding rule uses the (distinct)
+	set equality.  Workaround: supply a type instance of the rule that
+	creates new equalities (e.g. PartE in HOL/ex/Simult)
+	==> affects freeness reasoning about Sexp constants (since they have
+		type ... set)
+
   With substition for equalities (hyp_subst_tac):
     1.  Sometimes hyp_subst_tac will fail due to occurrence of the parameter
         as the argument of a function variable
@@ -297,7 +308,7 @@
 
 (*Normalize...but not the bodies of ABSTRACTIONS*)
 fun norm t = case t of
-    Skolem(a,args)       => Skolem(a, vars_in_vars args)
+    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
@@ -314,6 +325,13 @@
   | (f $ u) => (case wkNormAux f of
 		    Abs(_,body) => wkNorm (subst_bound (u, body))
 		  | nf          => nf $ u)
+  | Abs (a,body) =>	(*eta-contract if possible*)
+	(case wkNormAux body of
+	     nb as (f $ t) => 
+		 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
+		 then Abs(a,nb)
+		 else wkNorm (incr_boundvars ~1 f)
+	   | nb          => Abs (a,nb))
   | _ => t
 and wkNorm t = case head_of t of
     Const _        => t
@@ -630,7 +648,7 @@
      (map normLev br, map norm lits, vars, lim);
 
 fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace 
-		else ()
+	 	  else ()
 end;
 
 
@@ -740,9 +758,9 @@
   | addLit (G,lits) = ins_term(G, lits)
 
 
-(*For calculating the "penalty" to assess on a branching factor of n*)
-fun log2 1 = 0
-  | log2 n = 1 + log2(n div 2);
+(*For calculating the "penalty" to assess on a branching factor of n
+  log2 seems a little too severe*)
+fun log3 n = if n<3 then 0 else 1 + log3(n div 3);
 
 
 (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
@@ -781,7 +799,7 @@
 			    (*P comes from the rule; G comes from the branch.*)
                         val ntrl' = !ntrail
 			val lim' = if ntrl < !ntrail 
-				   then lim - (1+log2(length rules))
+				   then lim - (1+log3(length rules))
 				   else lim   (*discourage branching updates*)
                         val vars  = vars_in_vars vars
                         val vars' = foldr add_terms_vars (prems, vars)
@@ -879,7 +897,7 @@
                         val dup = md andalso vars' <> vars
 			(*duplicate H only if md and the premise has new vars*)
 			val lim' = (*Decrement "lim" extra if updates occur*)
-			    if ntrl < !ntrail then lim - (1+log2(length rules))
+			    if ntrl < !ntrail then lim - (1+log3(length rules))
 			    else lim-1
 			    (*NB: if the formula is duplicated, 
 			      then it seems plausible to leave lim alone.