# HG changeset patch
# User blanchet
# Date 1416500958 -3600
# Node ID b29281d6d1dbae25b61c13f39355c61024d7c082
# Parent  a86683d6c97e314875d8144c6cf5daf14146e46f
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)

diff -r a86683d6c97e -r b29281d6d1db src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Nov 20 17:29:18 2014 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Nov 20 17:29:18 2014 +0100
@@ -104,7 +104,7 @@
           | quant_name SMT_Translate.SExists = "exists"
 
         fun gen_trees_of_pat keyword ps =
-          [SMTLIB.Key keyword, (case map (tree_of_sterm l') ps of [t] => t | ts => SMTLIB.S ts)]
+          [SMTLIB.Key keyword, SMTLIB.S (map (tree_of_sterm l') ps)]
         fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
           | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
         fun tree_of_pats [] t = t