| changeset 16424 | 18a07ad8fea8 |
| parent 16366 | 6ff17d08c3d5 |
| child 16935 | 4d7f19d340e8 |
--- a/src/HOL/Tools/refute.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Tools/refute.ML Fri Jun 17 18:33:05 2005 +0200 @@ -183,8 +183,8 @@ parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; val copy = I; - val prep_ext = I; - fun merge + val extend = I; + fun merge _ ({interpreters = in1, printers = pr1, parameters = pa1}, {interpreters = in2, printers = pr2, parameters = pa2}) = {interpreters = rev (merge_alists (rev in1) (rev in2)),