src/Pure/thm.ML
changeset 3577 9715b6e3ec5f
parent 3565 c64410e701fb
child 3789 5802db941718
     1.1 --- a/src/Pure/thm.ML	Fri Jul 25 13:17:14 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 25 13:18:09 1997 +0200
     1.3 @@ -152,9 +152,11 @@
     1.4    val add_congs         : meta_simpset * thm list -> meta_simpset
     1.5    val del_congs         : meta_simpset * thm list -> meta_simpset
     1.6    val add_simprocs	: meta_simpset *
     1.7 -    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
     1.8 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
     1.9 +      -> meta_simpset
    1.10    val del_simprocs	: meta_simpset *
    1.11 -    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    1.12 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.13 +      -> meta_simpset
    1.14    val add_prems         : meta_simpset * thm list -> meta_simpset
    1.15    val prems_of_mss      : meta_simpset -> thm list
    1.16    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
    1.17 @@ -1449,7 +1451,8 @@
    1.18  
    1.19  type rrule = {thm: thm, lhs: term, perm: bool};
    1.20  type cong = {thm: thm, lhs: term};
    1.21 -type simproc = {name: string, proc: Sign.sg -> term -> thm option, lhs: cterm, id: stamp};
    1.22 +type simproc =
    1.23 + {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    1.24  
    1.25  fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
    1.26    {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
    1.27 @@ -1761,7 +1764,7 @@
    1.28      (4) simplification procedures
    1.29  *)
    1.30  
    1.31 -fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
    1.32 +fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
    1.33               (shypst,hypst,maxt,t,ders) =
    1.34    let
    1.35        val tsigt = #tsig(Sign.rep_sg signt);
    1.36 @@ -1821,7 +1824,7 @@
    1.37          | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
    1.38              if Pattern.matches tsigt (plhs, t) then
    1.39               (trace_term ("Trying procedure " ^ name ^ " on:") signt eta_t;
    1.40 -              case proc signt eta_t of
    1.41 +              case proc signt prems eta_t of
    1.42                  None => (trace "FAILED"; proc_rews eta_t ps)
    1.43                | Some raw_thm =>
    1.44                   (trace_thm ("Procedure " ^ name ^ " proved rewrite rule:") raw_thm;