# HG changeset patch
# User wenzelm
# Date 1436107165 -7200
# Node ID 4af8b9c2b52f3293fab7069b7d4c42a4b44c8b3b
# Parent  9173467ec5b6074a9188cc75d6ed5f2b7cb1a293
clarified context;

diff -r 9173467ec5b6 -r 4af8b9c2b52f src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Sun Jul 05 15:43:45 2015 +0200
+++ b/src/FOLP/ex/Nat.thy	Sun Jul 05 16:39:25 2015 +0200
@@ -82,7 +82,9 @@
 lemmas nat_congs = Suc_cong Plus_cong
 
 ML {*
-  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
+  val add_ss =
+    FOLP_ss addcongs @{thms nat_congs}
+    |> fold (addrew @{context}) @{thms add_0 add_Suc}
 *}
 
 schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
diff -r 9173467ec5b6 -r 4af8b9c2b52f src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sun Jul 05 15:43:45 2015 +0200
+++ b/src/FOLP/simp.ML	Sun Jul 05 16:39:25 2015 +0200
@@ -24,14 +24,14 @@
 end;
 
 
-infix 4 addrews addcongs delrews delcongs setauto;
+infix 4 addcongs delrews delcongs setauto;
 
 signature SIMP =
 sig
   type simpset
   val empty_ss  : simpset
   val addcongs  : simpset * thm list -> simpset
-  val addrews   : simpset * thm list -> simpset
+  val addrew    : Proof.context -> thm -> simpset -> simpset
   val delcongs  : simpset * thm list -> simpset
   val delrews   : simpset * thm list -> simpset
   val dest_ss   : simpset -> thm list * thm list
@@ -220,15 +220,13 @@
     in add_norms(congs,ccs,new_asms) end;
 
 fun normed_rews congs =
-  let val add_norms = add_norm_tags congs in
-    fn thm =>
+  let
+    val add_norms = add_norm_tags congs
+    fun normed ctxt thm =
       let
-        val ctxt =
-          Thm.theory_of_thm thm
-          |> Proof_Context.init_global
-          |> Variable.declare_thm thm;
+        val ctxt' = Variable.declare_thm thm ctxt;
       in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end
-  end;
+  in normed end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
 
@@ -241,7 +239,7 @@
         SS of {auto_tac: int -> tactic,
                congs: thm list,
                cong_net: thm Net.net,
-               mk_simps: thm -> thm list,
+               mk_simps: Proof.context -> thm -> thm list,
                simps: (thm * thm list) list,
                simp_net: thm Net.net}
 
@@ -259,14 +257,12 @@
 
 val insert_thms = fold_rev insert_thm_warn;
 
-fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
-let val thms = mk_simps thm
+fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
+let val thms = mk_simps ctxt thm
 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
       simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
 end;
 
-fun ss addrews thms = fold addrew thms ss;
-
 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
 let val congs' = thms @ congs;
 in SS{auto_tac=auto_tac, congs= congs',
diff -r 9173467ec5b6 -r 4af8b9c2b52f src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Sun Jul 05 15:43:45 2015 +0200
+++ b/src/FOLP/simpdata.ML	Sun Jul 05 16:39:25 2015 +0200
@@ -78,9 +78,9 @@
 
 val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
 
-val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
+val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews;
 
 
 val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
 
-val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
+val FOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) FOLP_rews;