# HG changeset patch
# User blanchet
# Date 1349427423 -7200
# Node ID 6279490e043873971d8710ad10db56af2365a502
# Parent  b2135b2730e8647e1bd21fb0230da994bbc8869c
newer versions of Z3 call it "Bool" not "bool"

diff -r b2135b2730e8 -r 6279490e0438 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Thu Oct 04 23:19:02 2012 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Oct 05 10:57:03 2012 +0200
@@ -127,9 +127,10 @@
 
 (** basic and additional constructors **)
 
-fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
+fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool}
   | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
-  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: delete*)
+  | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}  (*FIXME: legacy*)
+  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: legacy*)
   | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
 
 fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)