src/Tools/eqsubst.ML
changeset 60358 aebfbcab1eb8
parent 59642 929984c529d3
child 67149 e61557884799
     1.1 --- a/src/Tools/eqsubst.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4      * term (* outer term *)
     1.5  
     1.6    type searchinfo =
     1.7 -    theory
     1.8 +    Proof.context
     1.9      * int (* maxidx *)
    1.10      * Zipper.T (* focusterm to search under *)
    1.11  
    1.12 @@ -67,7 +67,7 @@
    1.13    * term; (* outer term *)
    1.14  
    1.15  type searchinfo =
    1.16 -  theory
    1.17 +  Proof.context
    1.18    * int (* maxidx *)
    1.19    * Zipper.T; (* focusterm to search under *)
    1.20  
    1.21 @@ -138,8 +138,8 @@
    1.22    end;
    1.23  
    1.24  (* Unification with exception handled *)
    1.25 -(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
    1.26 -fun clean_unify thy ix (a as (pat, tgt)) =
    1.27 +(* given context, max var index, pat, tgt; returns Seq of instantiations *)
    1.28 +fun clean_unify ctxt ix (a as (pat, tgt)) =
    1.29    let
    1.30      (* type info will be re-derived, maybe this can be cached
    1.31         for efficiency? *)
    1.32 @@ -148,7 +148,7 @@
    1.33      (* FIXME is it OK to ignore the type instantiation info?
    1.34         or should I be using it? *)
    1.35      val typs_unify =
    1.36 -      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
    1.37 +      SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix))
    1.38          handle Type.TUNIFY => NONE;
    1.39    in
    1.40      (case typs_unify of
    1.41 @@ -161,7 +161,7 @@
    1.42               Vartab.dest (Envir.term_env env));
    1.43            val initenv =
    1.44              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    1.45 -          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
    1.46 +          val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv
    1.47              handle ListPair.UnequalLengths => Seq.empty
    1.48                | Term.TERM _ => Seq.empty;
    1.49            fun clean_unify' useq () =
    1.50 @@ -181,10 +181,10 @@
    1.51     bound variables. New names have been introduced to make sure they are
    1.52     unique w.r.t all names in the term and each other. usednames' is
    1.53     oldnames + new names. *)
    1.54 -fun clean_unify_z thy maxidx pat z =
    1.55 +fun clean_unify_z ctxt maxidx pat z =
    1.56    let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
    1.57      Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
    1.58 -      (clean_unify thy maxidx (t, pat))
    1.59 +      (clean_unify ctxt maxidx (t, pat))
    1.60    end;
    1.61  
    1.62  
    1.63 @@ -230,8 +230,8 @@
    1.64        end;
    1.65    in Zipper.lzy_search sf_valid_td_lr end;
    1.66  
    1.67 -fun searchf_unify_gen f (thy, maxidx, z) lhs =
    1.68 -  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
    1.69 +fun searchf_unify_gen f (ctxt, maxidx, z) lhs =
    1.70 +  Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z);
    1.71  
    1.72  (* search all unifications *)
    1.73  val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
    1.74 @@ -271,7 +271,7 @@
    1.75         o Zipper.mktop
    1.76         o Thm.prop_of) conclthm
    1.77    in
    1.78 -    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
    1.79 +    ((cfvs, conclthm), (ctxt, maxidx, ft))
    1.80    end;
    1.81  
    1.82  (* substitute using an object or meta level equality *)
    1.83 @@ -345,23 +345,20 @@
    1.84      val th = Thm.incr_indexes 1 gth;
    1.85      val tgt_term = Thm.prop_of th;
    1.86  
    1.87 -    val thy = Thm.theory_of_thm th;
    1.88 -    val cert = Thm.global_cterm_of thy;
    1.89 -
    1.90      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    1.91 -    val cfvs = rev (map cert fvs);
    1.92 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
    1.93  
    1.94      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
    1.95      val asm_nprems = length (Logic.strip_imp_prems asmt);
    1.96  
    1.97 -    val pth = Thm.trivial (cert asmt);
    1.98 +    val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt);
    1.99      val maxidx = Thm.maxidx_of th;
   1.100  
   1.101      val ft =
   1.102        (Zipper.move_down_right (* trueprop *)
   1.103           o Zipper.mktop
   1.104           o Thm.prop_of) pth
   1.105 -  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
   1.106 +  in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end;
   1.107  
   1.108  (* prepare subst in every possible assumption *)
   1.109  fun prep_subst_in_asms ctxt i gth =