# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID eb1e31eb7449a4039fc8bb7aea3f755357008771
# Parent  5792d6bb4fb163aca2488f82a877bceb1128f740
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)

diff -r 5792d6bb4fb1 -r eb1e31eb7449 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/ATP.thy	Tue May 31 16:38:36 2011 +0200
@@ -7,7 +7,8 @@
 
 theory ATP
 imports Meson
-uses "Tools/ATP/atp_util.ML"
+uses "Tools/monomorph.ML"
+     "Tools/ATP/atp_util.ML"
      "Tools/ATP/atp_problem.ML"
      "Tools/ATP/atp_proof.ML"
      "Tools/ATP/atp_systems.ML"
diff -r 5792d6bb4fb1 -r eb1e31eb7449 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue May 31 16:38:36 2011 +0200
@@ -310,6 +310,7 @@
   Tools/int_arith.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 \