--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 15:19:07 2014 +0100
@@ -129,6 +129,17 @@
| ord => ord
in {weight = weight, precedence = precedence} end
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
+ [alias] => alias
+ | _ => type_enc)
+ val opts =
+ [] |> type_enc <> partial_typesN ? cons type_enc
+ |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+
exception METIS_UNPROVABLE of unit
(* Main function to start Metis proof and reconstruction *)