src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
@@ -159,6 +159,7 @@
 ML_file "Tools/SMT/z3_isar.ML"
 ML_file "Tools/SMT/smt_solver.ML"
 ML_file "Tools/SMT/cvc4_interface.ML"
+ML_file "Tools/SMT/cvc4_proof_parse.ML"
 ML_file "Tools/SMT/verit_proof.ML"
 ML_file "Tools/SMT/verit_isar.ML"
 ML_file "Tools/SMT/verit_proof_parse.ML"