# HG changeset patch
# User wenzelm
# Date 1207596320 -7200
# Node ID 4d77568cdb2845a46cc0b66b3a11b53def4955c3
# Parent  3a3a83493f007afa3fe23f869c60e228f173982a
abs_conv: extra argument for bound variable;

diff -r 3a3a83493f00 -r 4d77568cdb28 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 07 21:25:18 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 07 21:25:20 2008 +0200
@@ -578,7 +578,7 @@
 val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
 
 
-val binder_conv = Conv.arg_conv oo Conv.abs_conv
+fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
@@ -614,7 +614,7 @@
     val case_hyp_conv = K (case_hyp RS eq_reflection)
     local open Conv in 
     val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
-    val sih = fconv_rule (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+    val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
     end
           
     fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =