src/HOL/Library/Code_Abstract_Nat.thy
changeset 55757 9fc71814b8c1
parent 55415 05f5fdb8d093
child 56790 f54097170704
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 10:10:38 2014 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 11:57:52 2014 +0100
     1.3 @@ -50,8 +50,9 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 -fun remove_suc thy thms =
     1.8 +fun remove_suc ctxt thms =
     1.9    let
    1.10 +    val thy = Proof_Context.theory_of ctxt;
    1.11      val vname = singleton (Name.variant_list (map fst
    1.12        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    1.13      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));