Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
authorblanchet
Thu, 20 Nov 2014 17:29:18 +0100
changeset 59021 b29281d6d1db
parent 59020 a86683d6c97e
child 59022 fa7c419f04b4
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
src/HOL/Tools/SMT/smtlib_interface.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle