simplified prove_conv;
authorwenzelm
Wed Jul 12 21:19:14 2006 +0200 (2006-07-12)
changeset 2011390a8d14f3610
parent 20112 a25c5d283239
child 20114 a1bb4bc68ff3
simplified prove_conv;
src/HOL/Integ/int_arith1.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Jul 12 19:59:14 2006 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed Jul 12 21:19:14 2006 +0200
     1.3 @@ -92,14 +92,13 @@
     1.4  
     1.5  structure Bin_Simprocs =
     1.6    struct
     1.7 -  fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
     1.8 +  fun prove_conv tacs ctxt (_: thm list) (t, u) =
     1.9      if t aconv u then NONE
    1.10      else
    1.11        let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    1.12 -      in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
    1.13 +      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
    1.14  
    1.15    fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    1.16 -  fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
    1.17  
    1.18    fun prep_simproc (name, pats, proc) =
    1.19      Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
     2.1 --- a/src/ZF/arith_data.ML	Wed Jul 12 19:59:14 2006 +0200
     2.2 +++ b/src/ZF/arith_data.ML	Wed Jul 12 21:19:14 2006 +0200
     2.3 @@ -12,8 +12,7 @@
     2.4    val nat_cancel: simproc list
     2.5    (*tools for use in similar applications*)
     2.6    val gen_trans_tac: thm -> thm option -> tactic
     2.7 -  val prove_conv: string -> tactic list -> Proof.context ->
     2.8 -                  thm list -> string list -> term * term -> thm option
     2.9 +  val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
    2.10    val simplify_meta_eq: thm list -> simpset -> thm -> thm
    2.11    (*debugging*)
    2.12    structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
    2.13 @@ -68,13 +67,13 @@
    2.14  
    2.15  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
    2.16  
    2.17 -fun prove_conv name tacs ctxt hyps xs (t,u) =
    2.18 +fun prove_conv name tacs ctxt prems (t,u) =
    2.19    if t aconv u then NONE
    2.20    else
    2.21 -  let val hyps' = List.filter (not o is_eq_thm) hyps
    2.22 -      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    2.23 +  let val prems' = List.filter (not o is_eq_thm) prems
    2.24 +      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
    2.25          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    2.26 -  in SOME (hyps' MRS Goal.prove ctxt xs [] goal (K (EVERY tacs)))
    2.27 +  in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
    2.28        handle ERROR msg =>
    2.29          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    2.30    end;