lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.

--- a/src/Pure/IsaPlanner/isand.ML	Thu May 05 11:56:00 2005 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Thu May 05 11:58:59 2005 +0200
@@ -55,7 +55,7 @@
   val allify_conditions' :
       (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
   val assume_allified :
-      Sign.sg -> (string * Term.typ) list * (string * Term.sort) list 
+      Sign.sg -> (string * Term.sort) list * (string * Term.typ) list
       -> Term.term -> (Thm.cterm * Thm.thm)
 
   (* meta level fixed params (i.e. !! vars) *)
@@ -78,6 +78,8 @@
   val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
   val fix_vars_and_tvars : 
       Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
+  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
+  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
   val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
   val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
   val unfix_frees_and_tfrees :
@@ -173,8 +175,10 @@
 (* implicit types and term *)
 fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
 
-(* allified version of term, given frees and types to allify over *)
-fun assume_allified sgn (vs,tyvs) t = 
+(* allified version of term, given frees to allify over. Note that we
+only allify over the types on the given allified cterm, we can't do
+this for the theorem as we are not allowed type-vars in the hyp. *)
+fun assume_allified sgn (tyvs,vs) t = 
     let
       fun allify_var (vt as (n,ty),t)  = 
           (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
@@ -240,6 +244,31 @@
       val fixedfrees = map snd crenamings;
     in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
 
+fun fix_tvars_upto_idx ix th = 
+    let 
+      val sgn = Thm.sign_of_thm th;
+      val ctypify = Thm.ctyp_of sgn
+      val prop = (Thm.prop_of th);
+      val tvars = Term.term_tvars prop;
+      val ctyfixes = 
+          Library.mapfilter 
+            (fn (v as ((s,i),ty)) => 
+                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
+                else NONE) tvars;
+    in Thm.instantiate (ctyfixes, []) th end;
+fun fix_vars_upto_idx ix th = 
+    let 
+      val sgn = Thm.sign_of_thm th;
+      val ctermify = Thm.cterm_of sgn
+      val prop = (Thm.prop_of th);
+      val vars = map Term.dest_Var (Term.term_vars prop);
+      val cfixes = 
+          Library.mapfilter 
+            (fn (v as ((s,i),ty)) => 
+                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
+                else NONE) vars;
+    in Thm.instantiate ([], cfixes) th end;
+
 
 (* make free vars into schematic vars with index zero *)
  fun unfix_frees frees = 

--- a/src/Pure/IsaPlanner/term_lib.ML	Thu May 05 11:56:00 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Thu May 05 11:58:59 2005 +0200
@@ -147,6 +147,7 @@
   | ho_term_height (Abs(_,_,t)) = ho_term_height t
   | ho_term_height _ = 0;
 
+
 (* Higher order matching with exception handled *)
 (* returns optional instantiation *)
 fun clean_match tsig (a as (pat, t)) = 
@@ -174,14 +175,14 @@
         let 
       (* is it right to throw away the flexes? 
          or should I be using them somehow? *)
-          fun mk_insts (env,flexflexes) = 
+          fun mk_insts env = 
             (Vartab.dest (Envir.type_env env),
              Envir.alist_of env);
           val initenv = Envir.Envir {asol = Vartab.empty, 
                                      iTs = typinsttab, maxidx = ix2};
-          val useq = (Unify.unifiers (sgn,initenv,[a]))
-	      handle UnequalLengths => Seq.empty
-		   | Term.TERM _ => Seq.empty;
+          val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
+	            handle UnequalLengths => Seq.empty
+		               | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () = 
               (case (Seq.pull useq) of 
                  NONE => NONE