--- a/src/HOL/Tools/Metis/metis_translate.ML Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Apr 14 11:24:05 2011 +0200
@@ -641,8 +641,9 @@
| metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
metis_lit pos s [Metis_Term.Fn (s',[])]
-fun default_sort _ (TVar _) = false
- | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
+fun has_default_sort _ (TVar _) = false
+ | has_default_sort ctxt (TFree (x, s)) =
+ (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
fun metis_of_tfree tf =
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
@@ -660,8 +661,8 @@
type_literals_for_types types_sorts, old_skolems)
else
let
- val tylits = filter_out (default_sort ctxt) types_sorts
- |> type_literals_for_types
+ val tylits = types_sorts |> filter_out (has_default_sort ctxt)
+ |> type_literals_for_types
val mtylits =
if type_lits then map (metis_of_type_literals false) tylits else []
in