src/HOL/Library/Code_Abstract_Nat.thy
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59643 f3be9235503d
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -59,7 +59,7 @@
     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 = Thm.cterm_of thy (Var ((vname, 0), HOLogic.natT));
     1.8 +    val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
     1.9      val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
    1.10      val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
    1.11      fun find_vars ct = (case Thm.term_of ct of