# HG changeset patch
# User oheimb
# Date 879333776 -3600
# Node ID 96876d71eef5b4ff7c1b0ba51da0f30a66577b6b
# Parent  858b3ec2c9db81eac1747bd3379c98e830d40008
renamed split_prem_tac to split_asm_tac
split_asm_tac: simplification, debugged first_prem_is_disj

diff -r 858b3ec2c9db -r 96876d71eef5 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Nov 11 16:04:14 1997 +0100
+++ b/src/Provers/splitter.ML	Wed Nov 12 12:22:56 1997 +0100
@@ -284,8 +284,8 @@
 in split_tac end;
 
 
-fun mk_case_split_prem_tac split_tac disjE conjE exE contrapos 
-			   contrapos2 notnotD = 
+fun mk_case_split_asm_tac split_tac 
+			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
 let
 
 (*****************************************************************************
@@ -295,8 +295,8 @@
    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
-fun split_prem_tac []     = K no_tac
-  | split_prem_tac splits = 
+fun split_asm_tac []     = K no_tac
+  | split_asm_tac splits = 
   let fun const thm =
             (case concl_of thm of Const ("Trueprop",_)$
 				 (Const ("op =", _)$(Var _$t)$_) =>
@@ -310,25 +310,27 @@
 				 (Logic.strip_assums_hyp t);
 	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
 				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
+	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
+					first_prem_is_disj t
 	      |   first_prem_is_disj _ = false;
-	      fun flat_prems_tac j = SUBGOAL (fn (t,i) => 
+	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
 				   (if first_prem_is_disj t
 				    then EVERY[etac disjE i, rotate_tac ~1 i,
 					       rotate_tac ~1  (i+1),
 					       flat_prems_tac (i+1)]
 				    else all_tac) 
 				   THEN REPEAT (eresolve_tac [conjE,exE] i)
-				   THEN REPEAT (dresolve_tac [notnotD]   i)) j;
+				   THEN REPEAT (dresolve_tac [notnotD]   i)) i;
 	  in if n<0 then no_tac else DETERM (EVERY'
 		[rotate_tac n, etac contrapos2,
 		 split_tac splits, 
 		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
-		 SELECT_GOAL (flat_prems_tac 1)] i)
+		 flat_prems_tac] i)
 	  end;
   in SUBGOAL tac
   end;
 
-in split_prem_tac end;
+in split_asm_tac end;
 
 
 in
@@ -337,6 +339,6 @@
 
 fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
 
-val mk_case_split_prem_tac = mk_case_split_prem_tac;
+val mk_case_split_asm_tac = mk_case_split_asm_tac;
 
 end;