src/Pure/raw_simplifier.ML
changeset 61057 5f6a1e31f3ad
parent 60822 4f58f3662e7d
child 61090 16f7f9aa4263
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun Aug 30 20:57:34 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Aug 30 21:26:42 2015 +0200
     1.3 @@ -151,6 +151,10 @@
     1.4    fo: bool,         (*use first-order matching*)
     1.5    perm: bool};      (*the rewrite rule is permutative*)
     1.6  
     1.7 +fun trim_context_rrule ({thm, name, lhs, elhs, extra, fo, perm}: rrule) =
     1.8 +  {thm = Thm.trim_context thm, name = name, lhs = lhs, elhs = Thm.trim_context_cterm elhs,
     1.9 +    extra = extra, fo = fo, perm = perm};
    1.10 +
    1.11  (*
    1.12  Remarks:
    1.13    - elhs is used for matching,
    1.14 @@ -470,7 +474,7 @@
    1.15    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.16      let
    1.17        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
    1.18 -      val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, rrule2) rules;
    1.19 +      val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules;
    1.20      in (rules', prems, depth) end)
    1.21    handle Net.INSERT =>
    1.22      (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
    1.23 @@ -917,17 +921,21 @@
    1.24  
    1.25  fun rewritec (prover, maxt) ctxt t =
    1.26    let
    1.27 +    val thy = Proof_Context.theory_of ctxt;
    1.28      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt;
    1.29      val eta_thm = Thm.eta_conversion t;
    1.30      val eta_t' = Thm.rhs_of eta_thm;
    1.31      val eta_t = Thm.term_of eta_t';
    1.32      fun rew rrule =
    1.33        let
    1.34 -        val {thm, name, lhs, elhs, extra, fo, perm} = rrule
    1.35 +        val {thm = thm0, name, lhs, elhs = elhs0, extra, fo, perm} = rrule;
    1.36 +        val thm = Thm.transfer thy thm0;
    1.37 +        val elhs = Thm.transfer_cterm thy elhs0;
    1.38          val prop = Thm.prop_of thm;
    1.39          val (rthm, elhs') =
    1.40            if maxt = ~1 orelse not extra then (thm, elhs)
    1.41            else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
    1.42 +
    1.43          val insts =
    1.44            if fo then Thm.first_order_match (elhs', eta_t')
    1.45            else Thm.match (elhs', eta_t');