1.1 --- a/src/HOL/Product_Type.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -774,10 +774,32 @@
     1.4  fun gen_id_42 aG bG i = (aG i, bG i);
     1.5  *}
     1.6  
     1.7 -consts_code
     1.8 -  "Pair"    ("(_,/ _)")
     1.9 -  "fst"     ("fst")
    1.10 -  "snd"     ("snd")
    1.11 +code_alias
    1.12 +  "*" "Product_Type.*"
    1.13 +  "Pair" "Product_Type.Pair"
    1.14 +  "fst" "Product_Type.fst"
    1.15 +  "snd" "Product_Type.snd"
    1.16 +
    1.17 +code_primconst fst
    1.18 +ml {*
    1.19 +fun fst (x, y) = x;
    1.20 +*}
    1.21 +
    1.22 +code_primconst snd
    1.23 +ml {*
    1.24 +fun snd (x, y) = y;
    1.25 +*}
    1.26 +
    1.27 +code_syntax_tyco
    1.28 +  *
    1.29 +    ml (infix 2 "*")
    1.30 +    haskell (atom "(__,/ __)")
    1.31 +
    1.32 +code_syntax_const
    1.33 +  fst
    1.34 +    haskell (atom "fst")
    1.35 +  snd
    1.36 +    haskell (atom "snd")
    1.37  
    1.38  ML {*
    1.39