# HG changeset patch
# User wenzelm
# Date 1230892267 -3600
# Node ID 76af2a3c9d2803b418653e3dbb4ecf811181fd81
# Parent  5c71a6da989d04b1f7d0bab4bc4df73eed8d3dbc
fixed assumption proof;

diff -r 5c71a6da989d -r 76af2a3c9d28 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Fri Jan 02 00:21:59 2009 +0100
+++ b/src/FOLP/IFOLP.thy	Fri Jan 02 11:31:07 2009 +0100
@@ -339,6 +339,7 @@
   shows "?a : R"
   apply (insert assms(1) [unfolded ex1_def])
   apply (erule exE conjE | assumption | rule assms(1))+
+  apply (erule assms(2), assumption)
   done