| changeset 43111 | 61faa204c810 |
| parent 43030 | e1172791ad0d |
| child 43244 | db041e88a805 |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue May 31 17:05:44 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue May 31 17:15:14 2011 +0200 @@ -271,8 +271,8 @@ @{const_name "equal_bool_inst.equal_bool"}, @{const_name "ord_fun_inst.less_eq_fun"}, @{const_name "ord_fun_inst.less_fun"}, - @{const_name Metis.fequal}, @{const_name Meson.skolem}, + @{const_name ATP.fequal}, @{const_name transfer_morphism}, @{const_name enum_prod_inst.enum_all_prod}, @{const_name enum_prod_inst.enum_ex_prod}