src/Tools/case_product.ML
changeset 44045 2814ff2a6e3e
parent 42361 23f352990944
child 45375 7fe19930dfc9
     1.1 --- a/src/Tools/case_product.ML	Sun Jul 31 11:13:38 2011 -0700
     1.2 +++ b/src/Tools/case_product.ML	Mon Aug 01 12:08:53 2011 +0200
     1.3 @@ -90,9 +90,9 @@
     1.4  
     1.5  fun annotation thm1 thm2 =
     1.6    let
     1.7 -    val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
     1.8 -    val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
     1.9 -    val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
    1.10 +    val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
    1.11 +    val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
    1.12 +    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
    1.13    in
    1.14      Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
    1.15    end