abs_conv: extra argument for bound variable;
authorwenzelm
Mon Apr 07 21:25:20 2008 +0200 (2008-04-07)
changeset 265694d77568cdb28
parent 26568 3a3a83493f00
child 26570 dbc458262f4c
abs_conv: extra argument for bound variable;
src/HOL/Tools/function_package/fundef_core.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 07 21:25:18 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 07 21:25:20 2008 +0200
     1.3 @@ -578,7 +578,7 @@
     1.4  val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
     1.5  
     1.6  
     1.7 -val binder_conv = Conv.arg_conv oo Conv.abs_conv
     1.8 +fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
     1.9  
    1.10  fun mk_partial_induct_rule thy globals R complete_thm clauses =
    1.11      let
    1.12 @@ -614,7 +614,7 @@
    1.13      val case_hyp_conv = K (case_hyp RS eq_reflection)
    1.14      local open Conv in 
    1.15      val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
    1.16 -    val sih = fconv_rule (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
    1.17 +    val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
    1.18      end
    1.19            
    1.20      fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =