expand_proof now also takes an optional term describing the proposition
authorberghofe
Wed Jul 10 18:39:15 2002 +0200 (2002-07-10 ago)
changeset 13342915d4d004643
parent 13341 f15ed50d16cf
child 13343 3b2b18c58d80
expand_proof now also takes an optional term describing the proposition
of the theorem to be expanded (to avoid problems with different theorems
having the same names).
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Jul 10 18:37:51 2002 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 10 18:39:15 2002 +0200
     1.3 @@ -12,7 +12,8 @@
     1.4    val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
     1.5    val prop_of' : term list -> Proofterm.proof -> term
     1.6    val prop_of : Proofterm.proof -> term
     1.7 -  val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
     1.8 +  val expand_proof : Sign.sg -> (string * term option) list ->
     1.9 +    Proofterm.proof -> Proofterm.proof
    1.10  end;
    1.11  
    1.12  structure Reconstruct : RECONSTRUCT =
    1.13 @@ -330,7 +331,7 @@
    1.14    expand and reconstruct subproofs
    1.15  *********************************************************************************)
    1.16  
    1.17 -fun expand_proof sg names prf =
    1.18 +fun expand_proof sg thms prf =
    1.19    let
    1.20      fun expand maxidx prfs (AbsP (s, t, prf)) = 
    1.21            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    1.22 @@ -347,7 +348,10 @@
    1.23            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    1.24            in (maxidx', prfs', prf' % t) end
    1.25        | expand maxidx prfs (prf as PThm ((a, _), cprf, prop, Some Ts)) =
    1.26 -          if not (a mem names) then (maxidx, prfs, prf) else
    1.27 +          if not (exists
    1.28 +            (fn (b, None) => a = b
    1.29 +              | (b, Some prop') => a = b andalso prop = prop') thms)
    1.30 +          then (maxidx, prfs, prf) else
    1.31            let
    1.32              val (maxidx', (i, prf), prfs') = (case assoc (prfs, (a, prop)) of
    1.33                  None =>