# HG changeset patch
# User paulson
# Date 888229489 -3600
# Node ID f6298426f5a758819505d328ce933423b0401935
# Parent  f5f957ab73eb0c280868641b173f3758f129756d
Catches bad elim rules, handling exception OPTION

diff -r f5f957ab73eb -r f6298426f5a7 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Feb 23 11:16:18 1998 +0100
+++ b/src/Provers/classical.ML	Mon Feb 23 11:24:49 1998 +0100
@@ -205,8 +205,10 @@
 (*Duplication of hazardous rules, for complete provers*)
 fun dup_intr th = zero_var_indexes (th RS classical);
 
-fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> 
-                  rule_by_tactic (TRYALL (etac revcut_rl));
+fun dup_elim th = 
+    th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> 
+    rule_by_tactic (TRYALL (etac revcut_rl))
+    handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th);
 
 
 (**** Classical rule sets ****)
@@ -219,7 +221,7 @@
 	 uwrapper	: (int -> tactic) ->
 			  (int -> tactic),	(*for transforming step_tac*)
 	 swrapper	: (int -> tactic) ->
-			  (int -> tactic),	(*for transform. safe_step_tac*)
+			  (int -> tactic),	(*for safe_step_tac*)
 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)