ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
@@ -337,7 +337,7 @@
map (pair 0)
#> rpair ctxt
#-> Monomorph.monomorph Monomorph.all_schematic_consts_of
- #> fst #> maps (map snd))
+ #> fst #> maps (map (zero_var_indexes o 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} []