src/HOLCF/Tools/Domain/domain_library.ML
changeset 37145 01aa36932739
parent 36692 54b64d4ad524
child 37391 476270a6c2dc
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 17:41:27 2010 +0200
@@ -185,7 +185,7 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
 end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)