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 45551 a62c7a21f4ab
parent 45514 973bb7846505
child 45554 09ad83de849c 
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 06:50:05 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -230,7 +230,7 @@
                cat_lines (map (Syntax.string_of_term ctxt o snd) props))
     *)
     val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
-    val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
+    val (atp_problem, _, _, lifted, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
                           false false [] @{prop False} props
     (*
isabelle