# 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