--- a/src/HOLCF/domain/syntax.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Thu Jul 14 19:28:24 2005 +0200
@@ -105,8 +105,8 @@
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
- val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
val ctt = map (calc_syntax funprod) eqs';