src/HOLCF/domain/theorems.ML

         val (le1,le2) = (hd leqs, hd(tl leqs));
         val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
         if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
         if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
                                         [eq1, eq2] end;
+    open Basis_Library (*restore original List*)
     fun distincts []      = []
-    |   distincts ((c,leqs)::cs) = List_.concat
+    |   distincts ((c,leqs)::cs) = List.concat
 	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
 		    distincts cs;
     in distincts (cons~~distincts_le) end;
 
 local