--- a/src/HOLCF/domain/theorems.ML Sat Nov 01 13:00:31 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Nov 01 13:01:07 1997 +0100
@@ -267,8 +267,9 @@
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;