--- a/src/Tools/case_product.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/case_product.ML Wed Dec 16 16:31:36 2015 +0100
@@ -96,7 +96,8 @@
Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
end
-fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
+fun annotation thm1 thm2 =
+ Thm.rule_attribute [thm1, thm2] (K (annotation_rule thm1 thm2))
fun combine_annotated ctxt thm1 thm2 =
combine ctxt thm1 thm2
@@ -111,7 +112,7 @@
let
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
in
- Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+ Attrib.thms >> (fn thms => Thm.rule_attribute thms (fn ctxt => fn thm =>
combine_list (Context.proof_of ctxt) thms thm))
end
"product with other case rules")