src/Pure/drule.ML

--- a/src/Pure/drule.ML	Tue Nov 28 00:35:18 2006 +0100
+++ b/src/Pure/drule.ML	Tue Nov 28 00:35:21 2006 +0100
@@ -963,7 +963,7 @@
   in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
 
 fun dest_term th =
-  let val cprop = Thm.cprop_of th in
+  let val cprop = strip_imp_concl (Thm.cprop_of th) in
     if can Logic.dest_term (Thm.term_of cprop) then
       Thm.dest_arg cprop
     else raise THM ("dest_term", 0, [th])