src/HOL/Library/Code_Abstract_Nat.thy
changeset 59643 f3be9235503d
parent 59621 291934bac95e
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:56:43 2015 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:57:01 2015 +0100
     1.3 @@ -56,10 +56,9 @@
     1.4  
     1.5  fun remove_suc ctxt thms =
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt;
     1.8      val vname = singleton (Name.variant_list (map fst
     1.9        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    1.10 -    val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.11 +    val cv = Thm.cterm_of ctxt (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