src/HOL/Tools/refute.ML
changeset 21098 d0d8a48ae4e6
parent 21078 101aefd61aac
child 21267 5294ecae6708
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Oct 23 11:18:50 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Oct 23 16:49:21 2006 +0200
     1.3 @@ -187,8 +187,8 @@
     1.4  		fun merge _
     1.5  			({interpreters = in1, printers = pr1, parameters = pa1},
     1.6  			 {interpreters = in2, printers = pr2, parameters = pa2}) =
     1.7 -			{interpreters = rev (merge_alists (rev in1) (rev in2)),
     1.8 -			 printers = rev (merge_alists (rev pr1) (rev pr2)),
     1.9 +			{interpreters = AList.merge (op =) (K true) (in1, in2),
    1.10 +			 printers = AList.merge (op =) (K true) (pr1, pr2),
    1.11  			 parameters = Symtab.merge (op=) (pa1, pa2)};
    1.12  		fun print sg {interpreters, printers, parameters} =
    1.13  			Pretty.writeln (Pretty.chunks