src/HOL/Library/Code_Abstract_Nat.thy
changeset 59582 0fbed69ff081
parent 59169 ddc948e4ed09
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -59,10 +59,10 @@
     1.4      val thy = Proof_Context.theory_of ctxt;
     1.5      val vname = singleton (Name.variant_list (map fst
     1.6        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
     1.7 -    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
     1.8 -    val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o cprop_of;
     1.9 -    val rhs_of = snd o Thm.dest_comb o cprop_of;
    1.10 -    fun find_vars ct = (case term_of ct of
    1.11 +    val cv = Thm.cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.12 +    val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
    1.13 +    val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
    1.14 +    fun find_vars ct = (case Thm.term_of ct of
    1.15          (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.16        | _ $ _ =>
    1.17          let val (ct1, ct2) = Thm.dest_comb ct
    1.18 @@ -79,7 +79,7 @@
    1.19            Thm.implies_elim
    1.20             (Conv.fconv_rule (Thm.beta_conversion true)
    1.21               (Drule.instantiate'
    1.22 -               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    1.23 +               [SOME (Thm.ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    1.24                   SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
    1.25                 Suc_if_eq)) (Thm.forall_intr cv' thm)
    1.26        in
    1.27 @@ -97,7 +97,7 @@
    1.28  
    1.29  fun eqn_suc_base_preproc ctxt thms =
    1.30    let
    1.31 -    val dest = fst o Logic.dest_equals o prop_of;
    1.32 +    val dest = fst o Logic.dest_equals o Thm.prop_of;
    1.33      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.34    in
    1.35      if forall (can dest) thms andalso exists (contains_suc o dest) thms