tuned concat_with_and;
authorwenzelm
Wed Jul 13 16:07:22 2005 +0200 (2005-07-13)
changeset 168014bb13fa6ae72
parent 16800 90eff1b52428
child 16802 6eeee59dac4c
tuned concat_with_and;
improved Net interface;
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 13 16:07:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 13 16:07:22 2005 +0200
     1.3 @@ -86,9 +86,7 @@
     1.4    in  has  end;
     1.5  
     1.6  (* for tracing: encloses each string element in brackets. *)
     1.7 -fun concat_with_and [] = ""
     1.8 -  | concat_with_and [x] = "(" ^ x ^ ")"
     1.9 -  | concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs;
    1.10 +val concat_with_and = space_implode " & " o map (enclose "(" ")");
    1.11  
    1.12  
    1.13  (**** Clause handling ****)
    1.14 @@ -288,7 +286,7 @@
    1.15  (** Detecting repeated assumptions in a subgoal **)
    1.16  
    1.17  (*The stringtree detects repeated assumptions.*)
    1.18 -fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv);
    1.19 +fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
    1.20  
    1.21  (*detects repetitions in a list of terms*)
    1.22  fun has_reps [] = false