src/HOLCF/Tools/domain/domain_theorems.ML

         if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
         if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
           [eq1, eq2]
       end;
     fun distincts []      = []
-      | distincts ((c,leqs)::cs) = flat
-	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
-		    distincts cs;
+      | distincts ((c,leqs)::cs) =
+        flat
+          (ListPair.map (distinct c) ((map #1 cs),leqs)) @
+        distincts cs;
   in map standard (distincts (cons ~~ distincts_le)) end;
 
 local 
   fun pgterm rel con args =
     let