--- 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"),