src/HOL/Tools/refute.ML
changeset 21098 d0d8a48ae4e6
parent 21078 101aefd61aac
child 21267 5294ecae6708
equal deleted inserted replaced
21097:5a59f8ff96cc 21098:d0d8a48ae4e6
   185 		val copy = I;
   185 		val copy = I;
   186 		val extend = I;
   186 		val extend = I;
   187 		fun merge _
   187 		fun merge _
   188 			({interpreters = in1, printers = pr1, parameters = pa1},
   188 			({interpreters = in1, printers = pr1, parameters = pa1},
   189 			 {interpreters = in2, printers = pr2, parameters = pa2}) =
   189 			 {interpreters = in2, printers = pr2, parameters = pa2}) =
   190 			{interpreters = rev (merge_alists (rev in1) (rev in2)),
   190 			{interpreters = AList.merge (op =) (K true) (in1, in2),
   191 			 printers = rev (merge_alists (rev pr1) (rev pr2)),
   191 			 printers = AList.merge (op =) (K true) (pr1, pr2),
   192 			 parameters = Symtab.merge (op=) (pa1, pa2)};
   192 			 parameters = Symtab.merge (op=) (pa1, pa2)};
   193 		fun print sg {interpreters, printers, parameters} =
   193 		fun print sg {interpreters, printers, parameters} =
   194 			Pretty.writeln (Pretty.chunks
   194 			Pretty.writeln (Pretty.chunks
   195 				[Pretty.strs ("default parameters:" :: List.concat (map (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
   195 				[Pretty.strs ("default parameters:" :: List.concat (map (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
   196 				 Pretty.strs ("interpreters:" :: map fst interpreters),
   196 				 Pretty.strs ("interpreters:" :: map fst interpreters),