fix to subst in order to allow subst when head of a term is a bound variable.

--- a/src/Provers/IsaPlanner/zipper.ML	Mon Jul 03 17:17:41 2006 +0200
+++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jul 03 17:24:45 2006 +0200
@@ -91,17 +91,22 @@
   type T
 
   val mktop : C.D.Trm.T -> T
-  val goto_top : T -> T
+  val mk : (C.D.Trm.T * C.T) -> T
+
+  val goto_top : T -> T 
   val at_top : T -> bool
-  val mk : (C.D.Trm.T * C.T) -> T
-  val set_trm : C.D.Trm.T -> T -> T
-  val set_ctxt : C.T -> T -> T
 
   val split : T -> T * C.T
   val add_outerctxt : C.T -> T -> T
 
+  val set_trm : C.D.Trm.T -> T -> T
+  val set_ctxt : C.T -> T -> T
+
   val ctxt : T -> C.T
   val trm : T -> C.D.Trm.T
+  val top_trm : T -> C.D.Trm.T
+
+  val zipto : C.T -> T -> T (* follow context down *)
 
   val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
   val ty_ctxt : T -> C.D.Trm.typ list;
@@ -254,6 +259,7 @@
 
   val ctxt = snd;
   val trm = fst;
+  val top_trm = trm o goto_top;
 
   fun nty_ctxt x = C.nty_ctxt (ctxt x);
   fun ty_ctxt x = C.ty_ctxt (ctxt x);
@@ -321,10 +327,17 @@
       ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
     | move_down_app z = raise move ("move_down_app",z);
 
+  (* follow the given path down the given zipper *)
+  (* implicit arguments: C.D.dtrm list, then T *)
+  val zipto = 
+      C.fold (fn C.D.Abs _ => move_down_abs 
+               | C.D.AppL _ => move_down_left
+               | C.D.AppR _ => move_down_right) 
 
   (* Note: interpretted as being examined depth first *)
   datatype zsearch = Here of T | LookIn of T;
 
+  (* lazy search *)
   fun lzy_search fsearch = 
       let 
         fun lzyl [] () = NONE

--- a/src/Provers/eqsubst.ML	Mon Jul 03 17:17:41 2006 +0200
+++ b/src/Provers/eqsubst.ML	Mon Jul 03 17:24:45 2006 +0200
@@ -285,13 +285,13 @@
   | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   | bot_left_leaf_of x = x;
 
+(* Avoid considering replacing terms which have a var at the head as
+   they always succeed trivially, and uninterestingly. *)
 fun valid_match_start z =
     (case bot_left_leaf_of (Z.trm z) of 
-       Const _ => true
-     | Free _ => true
-     | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
-     | _ => false); (* avoid vars - always suceeds uninterestingly. *)
-                      
+      Var _ => false 
+      | _ => true);
+
 (* search from top, left to right, then down *)
 val search_lr_all = ZipperSearch.all_bl_ur;