src/HOL/Tools/Function/induction_schema.ML
changeset 59582 0fbed69ff081
parent 59580 cbc38731d42f
child 59618 e6939796717e
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -46,8 +46,8 @@
     1.4    (map meta (@{thm split_conv} :: @{thms sum.case}))
     1.5  
     1.6  fun term_conv thy cv t =
     1.7 -  cv (cterm_of thy t)
     1.8 -  |> prop_of |> Logic.dest_equals |> snd
     1.9 +  cv (Thm.cterm_of thy t)
    1.10 +  |> Thm.prop_of |> Logic.dest_equals |> snd
    1.11  
    1.12  fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    1.13  
    1.14 @@ -205,7 +205,7 @@
    1.15    (IndScheme {T, cases=scases, branches}) =
    1.16    let
    1.17      val thy = Proof_Context.theory_of ctxt
    1.18 -    val cert = cterm_of thy
    1.19 +    val cert = Thm.cterm_of thy
    1.20  
    1.21      val n = length branches
    1.22      val scases_idx = map_index I scases
    1.23 @@ -274,14 +274,14 @@
    1.24                  |> Conv.fconv_rule (sum_prod_conv ctxt)
    1.25                  |> Conv.fconv_rule (ind_rulify ctxt)
    1.26                  |> (fn th => th COMP ipres) (* P rs *)
    1.27 -                |> fold_rev (Thm.implies_intr o cprop_of) cGas
    1.28 +                |> fold_rev (Thm.implies_intr o Thm.cprop_of) cGas
    1.29                  |> fold_rev Thm.forall_intr cGvs
    1.30                end
    1.31  
    1.32              val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
    1.33  
    1.34              val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
    1.35 -              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
    1.36 +              |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
    1.37                |> fold_rev (curry Logic.mk_implies) gs
    1.38                |> fold_rev (Logic.all o Free) qs
    1.39                |> cert
    1.40 @@ -295,7 +295,7 @@
    1.41                |> fold Thm.elim_implies ags
    1.42                |> fold Thm.elim_implies P_recs (* P lhs *)
    1.43                |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
    1.44 -              |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
    1.45 +              |> fold_rev (Thm.implies_intr o Thm.cprop_of) (ags @ case_hyps)
    1.46                |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
    1.47            in
    1.48              (res, (cidx, step))
    1.49 @@ -308,7 +308,7 @@
    1.50            |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
    1.51            |> fold Thm.elim_implies C_hyps
    1.52            |> fold Thm.elim_implies cases (* P xs *)
    1.53 -          |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
    1.54 +          |> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps
    1.55            |> fold_rev (Thm.forall_intr o cert o Free) ws
    1.56  
    1.57          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
    1.58 @@ -319,7 +319,7 @@
    1.59            |> Seq.hd
    1.60            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
    1.61            |> Goal.finish ctxt
    1.62 -          |> Thm.implies_intr (cprop_of branch_hyp)
    1.63 +          |> Thm.implies_intr (Thm.cprop_of branch_hyp)
    1.64            |> fold_rev (Thm.forall_intr o cert) fxs
    1.65        in
    1.66          (Pxs, steps)
    1.67 @@ -380,7 +380,7 @@
    1.68        end
    1.69  
    1.70      val res = Conjunction.intr_balanced (map_index project branches)
    1.71 -      |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
    1.72 +      |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
    1.73        |> Drule.generalize ([], [Rn])
    1.74  
    1.75      val nbranches = length branches