# HG changeset patch
# User oheimb
# Date 905267259 -7200
# Node ID f68b9d225942f417f1dbaca29edc2aa78f4c6012
# Parent  cff7d1e9837635fac8b5010688966e63f71e4c3d
added caveat; a real solution would be difficult

diff -r cff7d1e98376 -r f68b9d225942 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Sep 08 17:03:21 1998 +0200
+++ b/src/Provers/splitter.ML	Tue Sep 08 17:07:39 1998 +0200
@@ -339,6 +339,7 @@
 	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
 					first_prem_is_disj t
 	      |   first_prem_is_disj _ = false;
+      (* does not work properly if the split variable is bound by a quantfier *)
 	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
 			   (if first_prem_is_disj t
 			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,