src/Pure/tctical.ML
changeset 5997 4d00bbd3d3ac
parent 5957 9c0c69ab7d02
child 6041 684ec6a1d802
equal deleted inserted replaced
5996:6b6e0ede3517 5997:4d00bbd3d3ac
   325                              handle Subscript => Seq.empty;
   325                              handle Subscript => Seq.empty;
   326 
   326 
   327 (*Returns all states that have changed in subgoal i, counted from the LAST
   327 (*Returns all states that have changed in subgoal i, counted from the LAST
   328   subgoal.  For stac, for example.*)
   328   subgoal.  For stac, for example.*)
   329 fun CHANGED_GOAL tac i st = 
   329 fun CHANGED_GOAL tac i st = 
   330     let val j = nprems_of st - i
   330     let val j = nprems_of st
   331         val t = List.nth(prems_of st, i-1)
   331         val t = List.nth(prems_of st, i-1)
   332         fun diff st' = 
   332         fun diff st' = (*true if subgoal still exists and is same as old one*)
   333 	    not (nprems_of st' > j   (*subgoal is still there*)
   333 	    not (nprems_of st' >= j
   334 		 andalso
   334 		 andalso
   335 		 t aconv List.nth(prems_of st', nprems_of st' - j - 1))
   335 		 Pattern.aeconv (t,
       
   336 				 List.nth(prems_of st', nprems_of st' - j)))
   336     in  Seq.filter diff (tac i st)  end
   337     in  Seq.filter diff (tac i st)  end
   337     handle Subscript => Seq.empty  (*no subgoal i*);
   338     handle Subscript => Seq.empty  (*no subgoal i*);
   338 
   339 
   339 fun ALLGOALS_RANGE tac (i:int) j st =
   340 fun ALLGOALS_RANGE tac (i:int) j st =
   340   if i > j then all_tac st
   341   if i > j then all_tac st