src/HOL/Tools/Function/induction_schema.ML
changeset 59058 a78612c67ec0
parent 58963 26bf09b95dda
child 59580 cbc38731d42f
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -339,7 +339,7 @@
     1.4        |> (curry op COMP) wf_thm
     1.5        |> (curry op COMP) istep
     1.6  
     1.7 -    val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
     1.8 +    val steps_sorted = map snd (sort (int_ord o apply2 fst) steps)
     1.9    in
    1.10      (steps_sorted, induct_rule)
    1.11    end
    1.12 @@ -356,8 +356,7 @@
    1.13      val x = Free (xn, ST)
    1.14      val cert = cterm_of (Proof_Context.theory_of ctxt)
    1.15  
    1.16 -    val ineqss = mk_ineqs R scheme
    1.17 -      |> map (map (pairself (Thm.assume o cert)))
    1.18 +    val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
    1.19      val complete =
    1.20        map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
    1.21      val wf_thm = mk_wf R scheme |> cert |> Thm.assume