- (fun (proof,opengoals) goal ->
- let newproof, newgoals = auto_tac mqi_handle (level-1) proof goal in
- (newproof, newgoals@opengoals))
- (proof,[]) goallist
+ (fun proof goal ->
+ (* It may happen that to close the first open goal
+ also some other goals are closed *)
+ let _,metasenv,_,_ = proof in
+ if List.exists (fun (i,_,_) -> i = goal) metasenv then
+ let newproof =
+ auto_tac mqi_handle (level-1) proof goal
+ in
+ newproof
+ else
+ (* goal already closed *)
+ proof)
+ proof goallist