--- a/src/HOL/ATP.thy Tue Aug 09 07:44:17 2011 +0200
+++ b/src/HOL/ATP.thy Tue Aug 09 09:05:21 2011 +0200
@@ -7,7 +7,8 @@
theory ATP
imports Meson
-uses "Tools/monomorph.ML"
+uses "Tools/lambda_lifting.ML"
+ "Tools/monomorph.ML"
"Tools/ATP/atp_util.ML"
"Tools/ATP/atp_problem.ML"
"Tools/ATP/atp_proof.ML"
--- a/src/HOL/IsaMakefile Tue Aug 09 07:44:17 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 09 09:05:21 2011 +0200
@@ -244,7 +244,9 @@
Tools/inductive_codegen.ML \
Tools/inductive_realizer.ML \
Tools/inductive_set.ML \
+ Tools/lambda_lifting.ML \
Tools/lin_arith.ML \
+ Tools/monomorph.ML \
Tools/nat_arith.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
@@ -309,10 +311,8 @@
Tools/code_evaluation.ML \
Tools/groebner.ML \
Tools/int_arith.ML \
- Tools/lambda_lifting.ML \
Tools/list_code.ML \
Tools/list_to_set_comprehension.ML \
- Tools/monomorph.ML \
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
--- a/src/HOL/SMT.thy Tue Aug 09 07:44:17 2011 +0200
+++ b/src/HOL/SMT.thy Tue Aug 09 09:05:21 2011 +0200
@@ -7,7 +7,6 @@
theory SMT
imports Record
uses
- "Tools/lambda_lifting.ML"
"Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_failure.ML"
"Tools/SMT/smt_config.ML"