tuned;
authorwenzelm
Tue Jun 04 20:01:02 2019 +0200 (6 weeks ago)
changeset 703259bf04a8f211f
parent 70324 005c1cdbfd3f
child 70326 aa7c49651f4e
tuned;
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Jun 04 19:51:45 2019 +0200
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Jun 04 20:01:02 2019 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5  (* instantiate generic fixpoint induction and eliminate the canonical assumptions;
     1.6    curry induction predicate *)
     1.7 -fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
     1.8 +fun specialize_fixp_induct ctxt fT fT_uc curry uncurry mono_thm f_def rule =
     1.9    let
    1.10      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
    1.11      val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
    1.12 @@ -186,14 +186,14 @@
    1.13  fun mk_curried_induct args ctxt inst_rule =
    1.14    let
    1.15      val cert = Thm.cterm_of ctxt
    1.16 +    (* FIXME ctxt vs. ctxt' (!?) *)
    1.17      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
    1.18  
    1.19      val split_paired_all_conv =
    1.20        Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
    1.21  
    1.22      val split_params_conv =
    1.23 -      Conv.params_conv ~1 (fn ctxt' =>
    1.24 -        Conv.implies_conv split_paired_all_conv Conv.all_conv)
    1.25 +      Conv.params_conv ~1 (fn _ => Conv.implies_conv split_paired_all_conv Conv.all_conv)
    1.26  
    1.27      val (P_var, x_var) =
    1.28         Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
    1.29 @@ -280,7 +280,7 @@
    1.30        |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
    1.31  
    1.32      val specialized_fixp_induct =
    1.33 -      specialize_fixp_induct lthy' args fT fT_uc F curry uncurry inst_mono_thm f_def fixp_induct
    1.34 +      specialize_fixp_induct lthy' fT fT_uc curry uncurry inst_mono_thm f_def fixp_induct
    1.35        |> Drule.rename_bvars' (map SOME (f_bname :: f_bname :: argnames));
    1.36  
    1.37      val mk_raw_induct =