--- a/src/HOL/hologic.ML Wed Oct 24 18:36:09 2007 +0200
+++ b/src/HOL/hologic.ML Wed Oct 24 19:21:38 2007 +0200
@@ -329,12 +329,11 @@
in ap [T] end;
-(***********************************************************)
-(* operations on tuples with specific arities *)
-(* *)
-(* an "arity" of a tuple is a list of lists of integers *)
-(* ("factors"), denoting paths to subterms that are pairs *)
-(***********************************************************)
+(* operations on tuples with specific arities *)
+(*
+ an "arity" of a tuple is a list of lists of integers
+ ("factors"), denoting paths to subterms that are pairs
+*)
fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);