# HG changeset patch
# User wenzelm
# Date 1188506138 -7200
# Node ID dc387e3999ecbe36f4a2b48b5fd2559e50eb0260
# Parent  d4380e9b287b94806248315eff3bdb2428ce4cf3
replaced ProofContext.infer_types by general Syntax.check_terms;
use Variable.polymorphic to get schematic type variables;

diff -r d4380e9b287b -r dc387e3999ec src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Aug 30 22:35:34 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Aug 30 22:35:38 2007 +0200
@@ -243,10 +243,9 @@
 
   fun fol_terms_to_hol ctxt fol_tms =
     let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
-        val _ = Output.debug (fn () => "  calling infer_types:")
+        val _ = Output.debug (fn () => "  calling type inference:")
         val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
-        val ts' = ProofContext.infer_types_pats ctxt ts
-                    (*DO NOT freeze TVars in the result*)
+        val ts' = Syntax.check_terms ctxt ts |> Variable.polymorphic ctxt;
         val _ = app (fn t => Output.debug
                       (fn () => "  final term: " ^ ProofContext.string_of_term ctxt t ^
                                 "  of type  " ^ ProofContext.string_of_typ ctxt (type_of t)))
@@ -309,7 +308,7 @@
         val _ = Output.debug (fn () => "  isa th: " ^ string_of_thm i_th)
         val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
         val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
-        val tms = ProofContext.infer_types_pats ctxt rawtms
+        val tms = Syntax.check_terms ctxt rawtms |> Variable.polymorphic ctxt;
         val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th)
         val substs' = ListPair.zip (vars, map ctm_of tms)
         val _ = Output.debug (fn() => "subst_translations:")