proper context;
authorwenzelm
Sun Dec 21 19:14:16 2014 +0100 (2014-12-21)
changeset 59169ddc948e4ed09
parent 59168 a5094641da6a
child 59170 de18f8b1a5a2
proper context;
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Tools/simpdata.ML
     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  
     2.1 --- a/src/HOL/Tools/simpdata.ML	Sun Dec 21 16:27:22 2014 +0100
     2.2 +++ b/src/HOL/Tools/simpdata.ML	Sun Dec 21 19:14:16 2014 +0100
     2.3 @@ -87,14 +87,15 @@
     2.4       else error "Conclusion of congruence rules must be =-equality"
     2.5     end);
     2.6  
     2.7 -fun mk_atomize pairs =
     2.8 +fun mk_atomize ctxt pairs =
     2.9    let
    2.10      fun atoms thm =
    2.11        let
    2.12          fun res th = map (fn rl => th RS rl);   (*exception THM*)
    2.13 +        val thm_ctxt = Variable.declare_thm thm ctxt;
    2.14          fun res_fixed rls =
    2.15            if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
    2.16 -          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
    2.17 +          else Variable.trade (K (fn [thm'] => res thm' rls)) thm_ctxt [thm];
    2.18        in
    2.19          case concl_of thm
    2.20            of Const (@{const_name Trueprop}, _) $ p => (case head_of p
    2.21 @@ -106,8 +107,8 @@
    2.22        end;
    2.23    in atoms end;
    2.24  
    2.25 -fun mksimps pairs (_: Proof.context) =
    2.26 -  map_filter (try mk_eq) o mk_atomize pairs o gen_all;
    2.27 +fun mksimps pairs ctxt =
    2.28 +  map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all;
    2.29  
    2.30  val simp_legacy_precond =
    2.31    Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)