dest_term: strip_imp_concl;
authorwenzelm
Tue Nov 28 00:35:21 2006 +0100 (2006-11-28)
changeset 21566af2932baf068
parent 21565 bd28361f4c5b
child 21567 c097a926ba78
dest_term: strip_imp_concl;
src/Pure/Isar/isar_cmd.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 28 00:35:18 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 28 00:35:21 2006 +0100
     1.3 @@ -193,7 +193,8 @@
     1.4  fun begin_theory name imports uses =
     1.5    ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
     1.6  
     1.7 -val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory;
     1.8 +fun end_theory thy =
     1.9 +  if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
    1.10  
    1.11  val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
    1.12  
     2.1 --- a/src/Pure/drule.ML	Tue Nov 28 00:35:18 2006 +0100
     2.2 +++ b/src/Pure/drule.ML	Tue Nov 28 00:35:21 2006 +0100
     2.3 @@ -963,7 +963,7 @@
     2.4    in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
     2.5  
     2.6  fun dest_term th =
     2.7 -  let val cprop = Thm.cprop_of th in
     2.8 +  let val cprop = strip_imp_concl (Thm.cprop_of th) in
     2.9      if can Logic.dest_term (Thm.term_of cprop) then
    2.10        Thm.dest_arg cprop
    2.11      else raise THM ("dest_term", 0, [th])