# HG changeset patch
# User wenzelm
# Date 1299163014 -3600
# Node ID 392364739e5d8cb130f638324b4330c1f93768a2
# Parent  ae8d62656392e9115677b90d947dd0b8cc12e7e0
observe standard header format;

diff -r ae8d62656392 -r 392364739e5d src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Thu Mar 03 15:19:20 2011 +0100
+++ b/src/Tools/case_product.ML	Thu Mar 03 15:36:54 2011 +0100
@@ -1,5 +1,5 @@
-(*   Title: case_product.ML
-     Author: Lars Noschinski
+(*  Title:      Tools/case_product.ML
+    Author:     Lars Noschinski, TU Muenchen
 
 Combines two case rules into a single one.
 
@@ -9,8 +9,7 @@
 *)
 
 signature CASE_PRODUCT =
-  sig
-
+sig
   val combine: Proof.context -> thm -> thm -> thm
   val combine_annotated: Proof.context -> thm -> thm -> thm
   val setup: theory -> theory
@@ -104,7 +103,8 @@
 
 (* Attribute setup *)
 
-val case_prod_attr = let
+val case_prod_attr =
+  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 =>