src/Pure/drule.ML
changeset 21566 af2932baf068
parent 21519 33f109ea389f
child 21578 a89f786b301a
     1.1 --- a/src/Pure/drule.ML	Tue Nov 28 00:35:18 2006 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Nov 28 00:35:21 2006 +0100
     1.3 @@ -963,7 +963,7 @@
     1.4    in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
     1.5  
     1.6  fun dest_term th =
     1.7 -  let val cprop = Thm.cprop_of th in
     1.8 +  let val cprop = strip_imp_concl (Thm.cprop_of th) in
     1.9      if can Logic.dest_term (Thm.term_of cprop) then
    1.10        Thm.dest_arg cprop
    1.11      else raise THM ("dest_term", 0, [th])