# HG changeset patch
# User haftmann
# Date 1256907762 -3600
# Node ID 85adf83af7ce1c93b82984ee31f17eae0694110d
# Parent  ee5b5ef5e970abcdf3d14dc0ea6130499824b97c# Parent  1f18de40b43f8166a2ceeb85ff9f43aa7cac14fb
merged

diff -r 1f18de40b43f -r 85adf83af7ce Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Fri Oct 30 14:00:43 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M4	Fri Oct 30 14:02:42 2009 +0100
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/polyml/polyml-5.2.1"
-  ML_SYSTEM="polyml-5.2.1"
+  POLYML_HOME="/home/polyml/polyml-svn"
+  ML_SYSTEM="polyml-experimental"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="--mutable 800 --immutable 2000"
diff -r 1f18de40b43f -r 85adf83af7ce Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Fri Oct 30 14:00:43 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M8	Fri Oct 30 14:02:42 2009 +0100
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/polyml/polyml-5.2.1"
-  ML_SYSTEM="polyml-5.2.1"
+  POLYML_HOME="/home/polyml/polyml-svn"
+  ML_SYSTEM="polyml-experimental"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="--mutable 800 --immutable 2000"
diff -r 1f18de40b43f -r 85adf83af7ce src/HOL/SMT/Examples/cert/z3_arith_quant_18
--- a/src/HOL/SMT/Examples/cert/z3_arith_quant_18	Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_18	Fri Oct 30 14:02:42 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 1f18de40b43f -r 85adf83af7ce src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Oct 30 14:02:42 2009 +0100
@@ -15,8 +15,7 @@
 val solver_name = "cvc3"
 val env_var = "CVC3_SOLVER"
 
-val options =
-  ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"]
+val options = ["-lang", "smtlib", "-output-lang", "presentation"]
 
 val is_sat = String.isPrefix "Satisfiable."
 val is_unsat = String.isPrefix "Unsatisfiable."
@@ -25,11 +24,7 @@
 fun cex_kind true = "Counterexample"
   | cex_kind false = "Possible counterexample"
 
-fun raise_cex real ctxt recon ls =
-  let
-    val ls' = filter_out (String.isPrefix "%") ls
-    val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls')
-  in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
 
 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
@@ -38,8 +33,8 @@
     val (l, ls) = split_first (dropwhile empty_line output)
   in
     if is_unsat l then @{cprop False}
-    else if is_sat l then raise_cex true context recon ls
-    else if is_unknown l then raise_cex false context recon ls
+    else if is_sat l then raise_cex true
+    else if is_unknown l then raise_cex false
     else error (solver_name ^ " failed")
   end
 
diff -r 1f18de40b43f -r 85adf83af7ce src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Fri Oct 30 14:02:42 2009 +0100
@@ -318,7 +318,7 @@
   fun replace ctxt cvs ct (cx as (nctxt, defs)) =
     let
       val cvs' = used_vars cvs ct
-      val ct' = fold Thm.cabs cvs' ct
+      val ct' = fold_rev Thm.cabs cvs' ct
       val mk_repl = fold (fn ct => fn cu => Thm.capply cu ct) cvs'
     in
       (case Termtab.lookup defs (Thm.term_of ct') of
diff -r 1f18de40b43f -r 85adf83af7ce src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Fri Oct 30 14:02:42 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)
diff -r 1f18de40b43f -r 85adf83af7ce src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Oct 30 14:02:42 2009 +0100
@@ -15,14 +15,12 @@
 val solver_name = "yices"
 val env_var = "YICES_SOLVER"
 
-val options = ["--evidence", "--smtlib"]
+val options = ["--smtlib"]
 
 fun cex_kind true = "Counterexample"
   | cex_kind false = "Possible counterexample"
 
-fun raise_cex real ctxt rtab ls =
-  let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
-  in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
 
 structure S = SMT_Solver
 
@@ -33,8 +31,8 @@
     val (l, ls) = split_first (dropwhile empty_line output)
   in
     if String.isPrefix "unsat" l then @{cprop False}
-    else if String.isPrefix "sat" l then raise_cex true context recon ls
-    else if String.isPrefix "unknown" l then raise_cex false context recon ls
+    else if String.isPrefix "sat" l then raise_cex true
+    else if String.isPrefix "unknown" l then raise_cex false
     else error (solver_name ^ " failed")
   end