Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_translate.ML
changeset 43132 44cd26bfc30c
parent 43130 d73fc2e55308
child 43159 29b55f292e0b 
--- 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} []
isabelle