# HG changeset patch
# User huffman
# Date 1269295520 25200
# Node ID 3d699b736ff4ca63e29718f5e8d22708e97368f9
# Parent  0c13e28e5e41cbf55e2130d184e0c4456dec314f
fix ML warning in domain_library.ML

diff -r 0c13e28e5e41 -r 3d699b736ff4 src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 14:58:21 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 15:05:20 2010 -0700
@@ -212,6 +212,7 @@
 fun con_app2 con f args = list_ccomb(%%:con,map f args);
 fun con_app con = con_app2 con %#;
 fun prj _  _  x (   _::[]) _ = x
+  | prj _  _  _ []         _ = error "Domain_Library.prj: empty list"
   | prj f1 _  x (_::y::ys) 0 = f1 x y
   | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;