1.1 --- a/src/Provers/eqsubst.ML	Sun Jun 01 17:39:21 2008 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Sun Jun 01 17:45:43 2008 +0200
     1.3 @@ -213,8 +213,9 @@
     1.4    let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
     1.5    in SOME (Vartab.dest tyenv, Vartab.dest tenv)
     1.6    end handle Pattern.MATCH => NONE;
     1.7 +
     1.8  (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
     1.9 -fun clean_unify sgn ix (a as (pat, tgt)) =
    1.10 +fun clean_unify thry ix (a as (pat, tgt)) =
    1.11      let
    1.12        (* type info will be re-derived, maybe this can be cached
    1.13           for efficiency? *)
    1.14 @@ -223,7 +224,7 @@
    1.15        (* is it OK to ignore the type instantiation info?
    1.16           or should I be using it? *)
    1.17        val typs_unify =
    1.18 -          SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
    1.19 +          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
    1.20              handle Type.TUNIFY => NONE;
    1.21      in
    1.22        case typs_unify of
    1.23 @@ -236,15 +237,15 @@
    1.24               Envir.alist_of env);
    1.25            val initenv = Envir.Envir {asol = Vartab.empty,
    1.26                                       iTs = typinsttab, maxidx = ix2};
    1.27 -          val useq = Unify.smash_unifiers sgn [a] initenv
    1.28 +          val useq = Unify.smash_unifiers thry [a] initenv
    1.29  	            handle UnequalLengths => Seq.empty
    1.30  		               | Term.TERM _ => Seq.empty;
    1.31            fun clean_unify' useq () =
    1.32                (case (Seq.pull useq) of
    1.33                   NONE => NONE
    1.34                 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
    1.35 -	      handle UnequalLengths => NONE
    1.36 -                   | Term.TERM _ => NONE;
    1.37 +	            handle UnequalLengths => NONE
    1.38 +                   | Term.TERM _ => NONE
    1.39          in
    1.40            (Seq.make (clean_unify' useq))
    1.41          end
    1.42 @@ -370,7 +371,7 @@
    1.43  
    1.44        val conclterm = Logic.strip_imp_concl fixedbody;
    1.45        val conclthm = trivify conclterm;
    1.46 -      val maxidx = Term.maxidx_of_term conclterm;
    1.47 +      val maxidx = Thm.maxidx_of th;
    1.48        val ft = ((Z.move_down_right (* ==> *)
    1.49                   o Z.move_down_left (* Trueprop *)
    1.50                   o Z.mktop
    1.51 @@ -487,7 +488,7 @@
    1.52        val asm_nprems = length (Logic.strip_imp_prems asmt);
    1.53  
    1.54        val pth = trivify asmt;
    1.55 -      val maxidx = Term.maxidx_of_term asmt;
    1.56 +      val maxidx = Thm.maxidx_of th;
    1.57  
    1.58        val ft = ((Z.move_down_right (* trueprop *)
    1.59                   o Z.mktop