dest_term: strip_imp_concl;

--- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 28 00:35:18 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 28 00:35:21 2006 +0100
@@ -193,7 +193,8 @@
 fun begin_theory name imports uses =
   ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
 
-val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory;
+fun end_theory thy =
+  if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
 
 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
 

--- 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])