src/Provers/classical.ML

--- a/src/Provers/classical.ML	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/Provers/classical.ML	Tue Jan 03 15:44:39 2006 +0100
@@ -262,12 +262,8 @@
 fun dup_intr th = zero_var_indexes (th RS classical);
 
 fun dup_elim th =
-  (case try (fn () =>
     rule_by_tactic (TRYALL (etac revcut_rl))
-      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd)) () of
-    SOME th' => th'
-  | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
-
+      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
 
 (**** Classical rule sets ****)
 
@@ -342,10 +338,10 @@
 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   assumptions.  Pairs elim rules with true. *)
 fun joinrules (intrs, elims) =
-  (map (pair true) (elims @ swapify intrs) @ map (pair false) intrs);
+  (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
 
 fun joinrules' (intrs, elims) =
-  (map (pair true) elims @ map (pair false) intrs);
+  map (pair true) elims @ map (pair false) intrs;
 
 (*Priority: prefer rules with fewest subgoals,
   then rules added most recently (preferring the head of the list).*)
@@ -419,6 +415,8 @@
   if mem_thm (th, safeEs) then
          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
           cs)
+  else if has_fewer_prems 1 th then
+    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   else
   let
       val th' = classical_rule th
@@ -445,6 +443,9 @@
 
 (*Give new theorem a name, if it has one already.*)
 fun name_make_elim th =
+    if has_fewer_prems 1 th then
+    	error("Ill-formed destruction rule\n" ^ string_of_thm th)
+    else
     case Thm.name_of_thm th of
         "" => Tactic.make_elim th
       | a  => Thm.name_thm (a ^ "_dest", Tactic.make_elim th);
@@ -475,7 +476,9 @@
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
         xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair}
-  end;
+  end
+  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
+         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
 
 fun addE th
   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
@@ -483,6 +486,8 @@
   if mem_thm (th, hazEs) then
          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
           cs)
+  else if has_fewer_prems 1 th then
+    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   else
   let
       val th' = classical_rule th
@@ -571,7 +576,10 @@
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
         xtra_netpair = delete' ([th], []) xtra_netpair}
- else cs;
+ else cs
+ handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
+        error ("Ill-formed introduction rule\n" ^ string_of_thm th);
+
 
 fun delE th
          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,