# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 8c9046951dcb6bef34fceeeac9c9ac92f209f439
# Parent  eb1e31eb7449a4039fc8bb7aea3f755357008771
monomorphize in the new Metis if the type system calls for it

diff -r eb1e31eb7449 -r 8c9046951dcb src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -320,7 +320,15 @@
     let
       val type_sys = type_sys |> the_default default_type_sys
       val explicit_apply = NONE
-      val clauses = conj_clauses @ fact_clauses
+      val clauses =
+        conj_clauses @ fact_clauses
+        |> (if polymorphism_of_type_sys type_sys = Polymorphic then
+              I
+            else
+              map (pair 0)
+              #> rpair ctxt
+              #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
+              #> fst #> maps (map snd))
       val (atp_problem, _, _, _, _, _, sym_tab) =
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
                             false false (map prop_of clauses) @{prop False} []