# HG changeset patch # User wenzelm # Date 1437936842 -7200 # Node ID 659117cc29635b2954fe2c9dd4e895788a267659 # Parent c6f96559e0325ebb6e459694774cdbff76670464 ignore non-existant variables, like other instantiate rules; diff -r c6f96559e032 -r 659117cc2963 src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Jul 26 17:32:59 2015 +0200 +++ b/src/Pure/drule.ML Sun Jul 26 20:54:02 2015 +0200 @@ -753,40 +753,38 @@ raise THM ("infer_instantiate: inconsistent types for variables " ^ commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), 0, [th]); - fun var_type xi = - (case AList.lookup (op =) vars xi of - SOME T => T - | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th])); - fun infer (xi, cu) (tyenv, maxidx) = - let - val T = var_type xi; - val U = Thm.typ_of_cterm cu; - val maxidx' = maxidx - |> Integer.max (#2 xi) - |> Term.maxidx_typ T - |> Integer.max (Thm.maxidx_of_cterm cu); - val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') - handle Type.TUNIFY => - let - val t = Var (xi, T); - val u = Thm.term_of cu; - in - raise THM ("infer_instantiate: type " ^ - Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ - Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ - "\ncannot be unified with type " ^ - Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ - Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), - 0, [th]) - end; - in (((xi, T), cu), (tyenv', maxidx'')) end; + fun infer (xi, cu) (inst, tyenv, maxidx) = + (case AList.lookup (op =) vars xi of + NONE => (inst, tyenv, maxidx) + | SOME T => + let + val U = Thm.typ_of_cterm cu; + val maxidx' = maxidx + |> Integer.max (#2 xi) + |> Term.maxidx_typ T + |> Integer.max (Thm.maxidx_of_cterm cu); + val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') + handle Type.TUNIFY => + let + val t = Var (xi, T); + val u = Thm.term_of cu; + in + raise THM ("infer_instantiate: type " ^ + Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ + Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ + "\ncannot be unified with type " ^ + Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ + Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), + 0, [th]) + end; + in (((xi, T), cu) :: inst, tyenv', maxidx'') end); - val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0); + val (inst0, tyenv, _) = fold infer args ([], Vartab.empty, 0); val instT = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; - val inst = args' |> map (fn ((xi, T), cu) => + val inst = inst0 |> map (fn ((xi, T), cu) => ((xi, Envir.norm_type tyenv T), Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); in instantiate_normalize (instT, inst) th end