# HG changeset patch
# User wenzelm
# Date 1164670521 -3600
# Node ID af2932baf0685c930888f5a01e704793368a9bf7
# Parent  bd28361f4c5b67f755638e4acca22a3d481efe37
dest_term: strip_imp_concl;

diff -r bd28361f4c5b -r af2932baf068 src/Pure/Isar/isar_cmd.ML
--- 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;
 
diff -r bd28361f4c5b -r af2932baf068 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])