--- a/src/HOL/SMT.thy Fri Oct 29 18:17:06 2010 +0200
+++ b/src/HOL/SMT.thy Fri Oct 29 18:17:08 2010 +0200
@@ -9,6 +9,7 @@
uses
"Tools/Datatype/datatype_selectors.ML"
("Tools/SMT/smt_monomorph.ML")
+ ("Tools/SMT/smt_builtin.ML")
("Tools/SMT/smt_normalize.ML")
("Tools/SMT/smt_translate.ML")
("Tools/SMT/smt_solver.ML")
@@ -126,6 +127,7 @@
subsection {* Setup *}
use "Tools/SMT/smt_monomorph.ML"
+use "Tools/SMT/smt_builtin.ML"
use "Tools/SMT/smt_normalize.ML"
use "Tools/SMT/smt_translate.ML"
use "Tools/SMT/smt_solver.ML"