src/HOL/SMT.thy
changeset 43929 61d432e51aff
parent 43928 24d6e759753f
child 44087 8e491cb8841c
--- a/src/HOL/SMT.thy	Wed Jul 20 09:23:12 2011 +0200
+++ b/src/HOL/SMT.thy	Wed Jul 20 12:23:20 2011 +0200
@@ -7,13 +7,13 @@
 theory SMT
 imports Record
 uses
+  "Tools/lambda_lifting.ML"
   "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_failure.ML"
   "Tools/SMT/smt_config.ML"
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_datatypes.ML")
   ("Tools/SMT/smt_normalize.ML")
-  ("Tools/lambda_lifting.ML")
   ("Tools/SMT/smt_translate.ML")
   ("Tools/SMT/smt_solver.ML")
   ("Tools/SMT/smtlib_interface.ML")
@@ -138,7 +138,6 @@
 use "Tools/SMT/smt_builtin.ML"
 use "Tools/SMT/smt_datatypes.ML"
 use "Tools/SMT/smt_normalize.ML"
-use "Tools/lambda_lifting.ML"
 use "Tools/SMT/smt_translate.ML"
 use "Tools/SMT/smt_solver.ML"
 use "Tools/SMT/smtlib_interface.ML"