author berghofe Wed, 10 Jul 2002 18:39:15 +0200 changeset 13342 915d4d004643 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).
```--- a/src/Pure/Proof/reconstruct.ML	Wed Jul 10 18:37:51 2002 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 10 18:39:15 2002 +0200
@@ -12,7 +12,8 @@
val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
-  val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
+  val expand_proof : Sign.sg -> (string * term option) list ->
+    Proofterm.proof -> Proofterm.proof
end;

structure Reconstruct : RECONSTRUCT =
@@ -330,7 +331,7 @@
expand and reconstruct subproofs
*********************************************************************************)

-fun expand_proof sg names prf =
+fun expand_proof sg thms prf =
let
fun expand maxidx prfs (AbsP (s, t, prf)) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
@@ -347,7 +348,10 @@
let val (maxidx', prfs', prf') = expand maxidx prfs prf
in (maxidx', prfs', prf' % t) end
| expand maxidx prfs (prf as PThm ((a, _), cprf, prop, Some Ts)) =
-          if not (a mem names) then (maxidx, prfs, prf) else
+          if not (exists
+            (fn (b, None) => a = b
+              | (b, Some prop') => a = b andalso prop = prop') thms)
+          then (maxidx, prfs, prf) else
let
val (maxidx', (i, prf), prfs') = (case assoc (prfs, (a, prop)) of
None =>```