--- a/src/HOL/IsaMakefile Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/IsaMakefile Wed May 12 23:53:57 2010 +0200
@@ -1245,11 +1245,11 @@
$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \
SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \
+ SMT/Tools/z3_interface.ML SMT/Tools/smt_additional_facts.ML \
SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
- SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML \
- SMT/Tools/smt_additional_facts.ML
+ SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT