# 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:")