# HG changeset patch
# User boehmes
# Date 1256898398 -3600
# Node ID 17d9c977f928431e46b2970f3e8f0e5eb43136d4
# Parent  021677ed8eaa6a87753a94d063ec9bae976dc973
pattern are separated only by spaces (no comma)

diff -r 021677ed8eaa -r 17d9c977f928 src/HOL/SMT/Examples/cert/z3_arith_quant_18
--- a/src/HOL/SMT/Examples/cert/z3_arith_quant_18	Fri Oct 30 10:42:39 2009 +0100
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_18	Fri Oct 30 11:26:38 2009 +0100
@@ -2,6 +2,6 @@
 :extrafuns (
   (uf_1 Int)
  )
-:assumption (not (forall (?x1 Int) (implies (< ?x1 uf_1) (< (* 2 ?x1) (* 2 uf_1))) :pat{ ?x1 }))
+:assumption (not (forall (?x1 Int) (implies (< ?x1 uf_1) (< (* 2 ?x1) (* 2 uf_1))) :pat { ?x1 }))
 :formula true
 )
diff -r 021677ed8eaa -r 17d9c977f928 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Fri Oct 30 10:42:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Fri Oct 30 11:26:38 2009 +0100
@@ -69,7 +69,6 @@
 
 fun wr1 s = sep (wr s)
 fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts))
-fun ins s f = (fn [] => I | x::xs => f x #> fold (fn x => wr1 s #> f x) xs)
 
 val term_marker = "__term"
 val formula_marker = "__form"
@@ -104,7 +103,7 @@
 
         val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
 
-        fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}"
+        fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
         fun wr_pat (T.SPat ts) = wrp "pat" ts
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)