# HG changeset patch # User krauss # Date 1372802909 -7200 # Node ID a1c4f586e3726d12d94a60d0d901cfd5b3a8fa5f # Parent c9a9359e028590efe9ba0e4565ad4623b82c8552 more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering diff -r c9a9359e0285 -r a1c4f586e372 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Wed Jul 03 00:08:29 2013 +0200 @@ -180,9 +180,10 @@ val inst_rule = cterm_instantiate' [SOME cuncurry, NONE, SOME ccurry] rule - val P_rangeT = + val (P_var, x_var) = Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop - |> Term.head_of |> Term.dest_Var |> snd |> range_type + |> strip_comb |> apsnd hd + val P_rangeT = range_type (snd (Term.dest_Var P_var)) val PT = map (snd o dest_Free) args ---> P_rangeT val x_inst = cert (foldl1 HOLogic.mk_prod args) val P_inst = cert (uncurry_n (length args) (Free (P, PT))) @@ -193,7 +194,7 @@ THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 THEN CONVERSION (split_params_conv ctxt then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) - |> Drule.instantiate' [] [NONE, NONE, SOME P_inst, SOME x_inst] + |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |> singleton (Variable.export ctxt' ctxt) in