src/HOL/Tools/nat_arith.ML
changeset 54742 7a86358a3c0b
parent 48571 d68b74435605
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  signature NAT_ARITH =
     1.6  sig
     1.7 -  val cancel_diff_conv: conv
     1.8 -  val cancel_eq_conv: conv
     1.9 -  val cancel_le_conv: conv
    1.10 -  val cancel_less_conv: conv
    1.11 +  val cancel_diff_conv: Proof.context -> conv
    1.12 +  val cancel_eq_conv: Proof.context -> conv
    1.13 +  val cancel_le_conv: Proof.context -> conv
    1.14 +  val cancel_less_conv: Proof.context -> conv
    1.15  end;
    1.16  
    1.17  structure Nat_Arith: NAT_ARITH =
    1.18 @@ -26,9 +26,9 @@
    1.19  
    1.20  val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
    1.21  
    1.22 -fun move_to_front path = Conv.every_conv
    1.23 +fun move_to_front ctxt path = Conv.every_conv
    1.24      [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    1.25 -     Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
    1.26 +     Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
    1.27  
    1.28  fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    1.29        add_atoms (add1::path) x #> add_atoms (add2::path) y
    1.30 @@ -54,12 +54,12 @@
    1.31      find (sort ord' xs) (sort ord' ys)
    1.32    end
    1.33  
    1.34 -fun cancel_conv rule ct =
    1.35 +fun cancel_conv rule ctxt ct =
    1.36    let
    1.37      val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    1.38      val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
    1.39 -    val lconv = move_to_front lpath
    1.40 -    val rconv = move_to_front rpath
    1.41 +    val lconv = move_to_front ctxt lpath
    1.42 +    val rconv = move_to_front ctxt rpath
    1.43      val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    1.44      val conv = conv1 then_conv Conv.rewr_conv rule
    1.45    in conv ct end