Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/z3_interface.ML
changeset 49720 6279490e0438
parent 47965 8ba6438557bc 
--- 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)
isabelle