# HG changeset patch
# User wenzelm
# Date 1121263642 -7200
# Node ID 4bb13fa6ae72705b3ade73208950073d5e000613
# Parent  90eff1b524282c144ab19ee172f100825e9930d1
tuned concat_with_and;
improved Net interface;

diff -r 90eff1b52428 -r 4bb13fa6ae72 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Jul 13 16:07:21 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jul 13 16:07:22 2005 +0200
@@ -86,9 +86,7 @@
   in  has  end;
 
 (* for tracing: encloses each string element in brackets. *)
-fun concat_with_and [] = ""
-  | concat_with_and [x] = "(" ^ x ^ ")"
-  | concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs;
+val concat_with_and = space_implode " & " o map (enclose "(" ")");
 
 
 (**** Clause handling ****)
@@ -288,7 +286,7 @@
 (** Detecting repeated assumptions in a subgoal **)
 
 (*The stringtree detects repeated assumptions.*)
-fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv);
+fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
 
 (*detects repetitions in a list of terms*)
 fun has_reps [] = false