diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 01 16:54:44 2010 +0200
@@ -96,13 +96,13 @@
 (* Readable names for the more common symbolic functions. Do not mess with the
    last nine entries of the table unless you know what you are doing. *)
 val const_trans_table =
-  Symtab.make [(@{type_name "*"}, "prod"),
-               (@{type_name "+"}, "sum"),
+  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
+               (@{type_name Sum_Type.sum}, "sum"),
                (@{const_name "op ="}, "equal"),
                (@{const_name "op &"}, "and"),
                (@{const_name "op |"}, "or"),
                (@{const_name "op -->"}, "implies"),
-               (@{const_name "op :"}, "in"),
+               (@{const_name Set.member}, "in"),
                (@{const_name fequal}, "fequal"),
                (@{const_name COMBI}, "COMBI"),
                (@{const_name COMBK}, "COMBK"),