# HG changeset patch
# User wenzelm
# Date 931635717 -7200
# Node ID 0c894ad534579609e90f745676e1cec8235bdb9b
# Parent  6109bcedbe1acf843e4fc71dd862d788567f0377
defer_tac: use try for general exn handling;

diff -r 6109bcedbe1a -r 0c894ad53457 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Jul 10 21:41:05 1999 +0200
+++ b/src/Pure/tactic.ML	Sat Jul 10 21:41:57 1999 +0200
@@ -111,16 +111,19 @@
   an old proof script, when the proof of an early subgoal fails.
   DOES NOT WORK FOR TYPE VARIABLES.
   Similar to drule/rotate_prems*)
-fun defer_tac i state = 
+fun defer_rule i state =
     let val (state',thaw) = freeze_thaw state
 	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
 	val hyp::hyps' = List.drop(hyps, i-1)
     in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
         |> implies_intr_list (List.take(hyps, i-1) @ hyps')
         |> thaw
-        |> Seq.single
-    end
-    handle _ => Seq.empty;
+    end;
+
+fun defer_tac i state =
+  (case try (defer_rule i) state of
+    Some state' => Seq.single state'
+  | None => Seq.empty);
 
 
 (*Makes a rule by applying a tactic to an existing rule*)