src/ZF/arith_data.ML
changeset 20044 92cc2f4c7335
parent 19250 932a50e2332f
child 20113 90a8d14f3610
     1.1 --- a/src/ZF/arith_data.ML	Sat Jul 08 12:54:29 2006 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Sat Jul 08 12:54:30 2006 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    val nat_cancel: simproc list
     1.5    (*tools for use in similar applications*)
     1.6    val gen_trans_tac: thm -> thm option -> tactic
     1.7 -  val prove_conv: string -> tactic list -> theory ->
     1.8 +  val prove_conv: string -> tactic list -> Proof.context ->
     1.9                    thm list -> string list -> term * term -> thm option
    1.10    val simplify_meta_eq: thm list -> simpset -> thm -> thm
    1.11    (*debugging*)
    1.12 @@ -68,13 +68,13 @@
    1.13  
    1.14  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
    1.15  
    1.16 -fun prove_conv name tacs sg hyps xs (t,u) =
    1.17 +fun prove_conv name tacs ctxt hyps xs (t,u) =
    1.18    if t aconv u then NONE
    1.19    else
    1.20    let val hyps' = List.filter (not o is_eq_thm) hyps
    1.21        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    1.22          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    1.23 -  in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
    1.24 +  in SOME (hyps' MRS Goal.prove ctxt xs [] goal (K (EVERY tacs)))
    1.25        handle ERROR msg =>
    1.26          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    1.27    end;
    1.28 @@ -205,17 +205,17 @@
    1.29       ["l #+ m = n", "l = m #+ n",
    1.30        "l #* m = n", "l = m #* n",
    1.31        "succ(m) = n", "m = succ(n)"],
    1.32 -     EqCancelNumerals.proc),
    1.33 +     (K EqCancelNumerals.proc)),
    1.34      ("natless_cancel_numerals",
    1.35       ["l #+ m < n", "l < m #+ n",
    1.36        "l #* m < n", "l < m #* n",
    1.37        "succ(m) < n", "m < succ(n)"],
    1.38 -     LessCancelNumerals.proc),
    1.39 +     (K LessCancelNumerals.proc)),
    1.40      ("natdiff_cancel_numerals",
    1.41       ["(l #+ m) #- n", "l #- (m #+ n)",
    1.42        "(l #* m) #- n", "l #- (m #* n)",
    1.43        "succ(m) #- n", "m #- succ(n)"],
    1.44 -     DiffCancelNumerals.proc)];
    1.45 +     (K DiffCancelNumerals.proc))];
    1.46  
    1.47  end;
    1.48