major_prem_of: Logic.strip_assums_concl;
authorwenzelm
Thu Oct 04 23:27:01 2001 +0200 (2001-10-04)
changeset 116926d15ae4b1123
parent 11691 fc9bd420162c
child 11693 63b0b2ec5830
major_prem_of: Logic.strip_assums_concl;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Oct 04 16:09:12 2001 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 04 23:27:01 2001 +0200
     1.3 @@ -358,7 +358,7 @@
     1.4  
     1.5  fun major_prem_of thm =
     1.6    (case prems_of thm of
     1.7 -    prem :: _ => prem
     1.8 +    prem :: _ => Logic.strip_assums_concl prem
     1.9    | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));
    1.10  
    1.11  fun no_prems thm = nprems_of thm = 0;