# HG changeset patch
# User paulson
# Date 826550016 -3600
# Node ID 70dd38777109a5be38cda0ea3ebdda77d9298c42
# Parent  822575c737bd96dd78d7bb318f2419fe465026d9
Made an exception handler more specific

diff -r 822575c737bd -r 70dd38777109 src/Pure/goals.ML
--- 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