# HG changeset patch
# User wenzelm
# Date 963774032 -7200
# Node ID 78a11a3534737089b39f8acceb62837e49a30309
# Parent  7834e56e22772340e23ac577e9f78bdf54aba111
strip_prod_type = HOLogic.prodT_factors;

diff -r 7834e56e2277 -r 78a11a353473 TFL/usyntax.sml
--- a/TFL/usyntax.sml	Sun Jul 16 21:00:10 2000 +0200
+++ b/TFL/usyntax.sml	Sun Jul 16 21:00:32 2000 +0200
@@ -38,9 +38,7 @@
 val alpha  = mk_vartype "'a"
 val beta   = mk_vartype "'b"
 
-fun strip_prod_type (Type("*", [ty1,ty2])) =
-	strip_prod_type ty1 @ strip_prod_type ty2
-  | strip_prod_type ty = [ty];
+val strip_prod_type = HOLogic.prodT_factors;
 
 
 
@@ -114,7 +112,7 @@
    in list_comb(c,[disj1,disj2])
    end;
 
-fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]);
+fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
 
 local
 fun mk_uncurry(xt,yt,zt) =