# HG changeset patch
# User haftmann
# Date 1369985432 -7200
# Node ID 35a2668ac3b0a8af87472e9cfb899aa5a85e3c3e
# Parent  3d7472b6b720ad383f9da93fc8a35019e5cc1fa1
permit multiple variable arguments in reflect

diff -r 3d7472b6b720 -r 35a2668ac3b0 src/HOL/Tools/reflection.ML
--- a/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
@@ -287,14 +287,16 @@
     val reify_thm = reify ctxt eqs t;
     fun try_corr corr_thm =
       SOME (FWD trans [reify_thm, corr_thm RS sym]) handle THM _ => NONE;
-    val thm = case get_first try_corr corr_thms
+    val refl_thm = case get_first try_corr corr_thms
      of NONE => error "No suitable correctness theorem found"
       | SOME thm => thm;
-    val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) thm;
-    val rth = conv ft;
+    val rhs = (Thm.dest_arg o Thm.dest_arg o cprop_of) refl_thm;
+    val number_of_args = (length o snd o strip_comb o term_of) rhs;
+    val reified = Thm.dest_arg (fold_range (K Thm.dest_fun) (number_of_args - 1) rhs);
+    val evaluated = conv reified;
   in
-    thm
-    |> simplify (put_simpset HOL_basic_ss ctxt addsimps [rth])
+    refl_thm
+    |> simplify (put_simpset HOL_basic_ss ctxt addsimps [evaluated])
     |> simplify (put_simpset HOL_basic_ss ctxt addsimps eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
   end;