--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Dec 31 00:11:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Jan 03 16:22:08 2011 +0100
@@ -851,7 +851,8 @@
|> tap (check_after idx r ps prop)
in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
- val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive}]
+ val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive},
+ Z3_Proof_Literals.true_thm]
fun all_disch_rules rules = map (pair false) (disch_rules @ rules)
fun disch_assm rules thm =