Made an exception handler more specific

--- a/src/Pure/goals.ML	Mon Mar 11 14:09:50 1996 +0100
+++ b/src/Pure/goals.ML	Mon Mar 11 14:13:36 1996 +0100
@@ -129,7 +129,7 @@
 	checks (if requested) that resulting theorem is equivalent to goal. *)
       fun mkresult (check,state) =
         let val state = Sequence.hd (flexflex_rule state)
-	    		handle _ => state   (*smash flexflex pairs*)
+	    		handle THM _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
             val th = strip_shyps (implies_intr_list cAs state)
             val {hyps,prop,sign=sign',...} = rep_thm th