# HG changeset patch
# User wenzelm
# Date 1188578794 -7200
# Node ID 5e135602f6605114a3faebc8f9a10d5a4ac00809
# Parent  5a3ee202e0b01d3246446112fc50dae6e9306d5b
type_infer: mode_pattern;

diff -r 5a3ee202e0b0 -r 5e135602f660 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Fri Aug 31 18:46:33 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Fri Aug 31 18:46:34 2007 +0200
@@ -159,18 +159,10 @@
 (*Instantiate constant c with the supplied types, but if they don't match its declared
   sort constraints, replace by a general type.*)
 fun const_of ctxt (c,Ts) =  Const (c, dummyT)
-(*Formerly, this code was used. Now, we just leave it all to type inference!
-  let val thy = ProofContext.theory_of ctxt
-      and (types, sorts) = Variable.constraints_of ctxt
-      val declaredT = Consts.the_constraint (Sign.consts_of thy) c
-      val t = Recon.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts)))
-  in
-      Sign.typ_match thy (declaredT, type_of t) Vartab.empty;
-      t
-  end
-  handle Type.TYPE_MATCH => Const (c, dummyT);
-*)
 
+fun infer_types ctxt =
+  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
+  
   (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
     with variable constraints in the goal...at least, type inference often fails otherwise.
     SEE ALSO axiom_inf below.*)
@@ -245,7 +237,7 @@
     let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
         val _ = Output.debug (fn () => "  calling type inference:")
         val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
-        val ts' = Syntax.check_terms ctxt ts |> Variable.polymorphic ctxt;
+        val ts' = infer_types ctxt ts;
         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)))
@@ -308,7 +300,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 = Syntax.check_terms ctxt rawtms |> Variable.polymorphic ctxt;
+        val tms = infer_types ctxt rawtms;
         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:")