1.1 --- a/src/HOLCF/Representable.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOLCF/Representable.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4  
     1.5  text "Cartesian products of representable types are representable."
     1.6  
     1.7 -instantiation "*" :: (rep, rep) rep
     1.8 +instantiation prod :: (rep, rep) rep
     1.9  begin
    1.10  
    1.11  definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
    1.12 @@ -763,7 +763,7 @@
    1.13       (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
    1.14          @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
    1.15  
    1.16 -     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
    1.17 +     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
    1.18          @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
    1.19  
    1.20       (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},