--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 15 13:49:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 15 13:57:17 2010 +0200
@@ -69,9 +69,9 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
- | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
- | hol_type_to_fol (Comp (tc, tps)) =
+fun hol_type_to_fol (TyVar x) = Metis.Term.Var x
+ | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, [])
+ | hol_type_to_fol (TyConstr (tc, tps)) =
Metis.Term.Fn (tc, map hol_type_to_fol tps);
(*These two functions insert type literals before the real literals. That is the