src/Tools/case_product.ML
changeset 67522 9e712280cc37
parent 67149 e61557884799
     1.1 --- a/src/Tools/case_product.ML	Sun Jan 28 16:09:00 2018 +0100
     1.2 +++ b/src/Tools/case_product.ML	Sun Jan 28 19:28:52 2018 +0100
     1.3 @@ -48,8 +48,8 @@
     1.4      val concl = Thm.concl_of thm1
     1.5  
     1.6      fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
     1.7 -    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
     1.8 -    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
     1.9 +    val (p_cons1, p_cases1) = chop_prefix is_consumes (Thm.prems_of thm1)
    1.10 +    val (p_cons2, p_cases2) = chop_prefix is_consumes (Thm.prems_of thm2)
    1.11  
    1.12      val p_cases_prod = map (fn p1 => map (fn p2 =>
    1.13        let