src/HOLCF/domain/syntax.ML
changeset 16842 5979c46853d1
parent 16394 495dbcd4f4c9
child 17811 10ebcd7032c1
--- 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';