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