src/HOL/Library/Code_Abstract_Nat.thy
changeset 59169 ddc948e4ed09
parent 58881 b9556a055632
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Sun Dec 21 16:27:22 2014 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sun Dec 21 19:14:16 2014 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4          case map_filter (fn thm'' =>
     1.5              SOME (thm'', singleton
     1.6                (Variable.trade (K (fn [thm'''] => [thm''' RS thm']))
     1.7 -                (Variable.global_thm_context thm'')) thm'')
     1.8 +                (Variable.declare_thm thm'' ctxt)) thm'')
     1.9            handle THM _ => NONE) thms of
    1.10              [] => NONE
    1.11            | thmps =>
    1.12 @@ -95,13 +95,13 @@
    1.13        end
    1.14    in get_first mk_thms eqs end;
    1.15  
    1.16 -fun eqn_suc_base_preproc thy thms =
    1.17 +fun eqn_suc_base_preproc ctxt thms =
    1.18    let
    1.19      val dest = fst o Logic.dest_equals o prop_of;
    1.20      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.21    in
    1.22      if forall (can dest) thms andalso exists (contains_suc o dest) thms
    1.23 -      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
    1.24 +      then thms |> perhaps_loop (remove_suc ctxt) |> (Option.map o map) Drule.zero_var_indexes
    1.25         else NONE
    1.26    end;
    1.27