diff -r 39ae45d3a11b -r 2b8e387d2dfc Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_library.ML	Thu Jun 16 20:07:03 2011 +0100
@@ -479,8 +479,10 @@
 
 (*
  inductive premises can be of the form
- R ... /\ P ...; split_conj_i picks out
- the part R or P part
+
+     R ... /\ P ...; 
+ 
+ split_conj_i picks out the part R or P part
 *)
 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = 
   (case head_of f1 of