attribute: Context.mapping;

--- a/src/HOL/Import/hol4rews.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Import/hol4rews.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -258,9 +258,8 @@
 val hol4_debug = ref false
 fun message s = if !hol4_debug then writeln s else ()
 
-fun add_hol4_rewrite (context, th) =
+fun add_hol4_rewrite (Context.Theory thy, th) =
     let
-        val thy = Context.the_theory context;
 	val _ = message "Adding HOL4 rewrite"
 	val th1 = th RS eq_reflection
 	val current_rews = HOL4Rewrites.get thy
@@ -268,7 +267,8 @@
 	val updated_thy  = HOL4Rewrites.put new_rews thy
     in
 	(Context.Theory updated_thy,th1)
-    end;
+    end
+  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
 
 fun ignore_hol4 bthy bthm thy =
     let

--- a/src/HOL/Import/shuffler.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -681,7 +681,7 @@
 	else ShuffleData.put (thm::shuffles) thy
     end
 
-val shuffle_attr = Thm.declaration_attribute (Context.map_theory o add_shuffle_rule);
+val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
 
 val setup =
   Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>

--- a/src/HOL/Tools/inductive_codegen.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -47,7 +47,7 @@
 
 fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
 
-fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
+fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
   let
     val {intros, graph, eqns} = CodegenData.get thy;
     fun thyname_of s = (case optmod of
@@ -71,7 +71,7 @@
                (s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
       | _ => (warn thm; thy))
     | _ => (warn thm; thy))
-  end));
+  end) I);
 
 fun get_clauses thy s =
   let val {intros, graph, ...} = CodegenData.get thy

--- a/src/HOL/Tools/inductive_realizer.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -467,7 +467,7 @@
     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   end
 
-fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
+fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
   let
     fun err () = error "ind_realizer: bad rule";
     val sets =
@@ -480,7 +480,7 @@
       (case arg of
         NONE => sets | SOME NONE => []
       | SOME (SOME sets') => sets \\ sets')
-  end);
+  end I);
 
 val ind_realizer = Attrib.syntax
  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--

--- a/src/HOL/Tools/recfun_codegen.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -36,7 +36,7 @@
 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
   string_of_thm thm);
 
-fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory
+fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping
   let
     fun add thm =
       if Pattern.pattern (lhs_of thm) then
@@ -47,7 +47,7 @@
   in
     add thm
     #> CodegenData.add_func thm
-  end);
+  end I);
 
 fun del_thm thm thy =
   let
@@ -60,7 +60,7 @@
   end handle TERM _ => (warn thm; thy);
 
 val del = Thm.declaration_attribute
-  (fn thm => Context.map_theory (del_thm thm #> CodegenData.del_func thm))
+  (fn thm => Context.mapping (del_thm thm #> CodegenData.del_func thm) I)
 
 fun del_redundant thy eqs [] = eqs
   | del_redundant thy eqs (eq :: eqs') =

--- a/src/HOL/arith_data.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/HOL/arith_data.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -231,8 +231,8 @@
 end);
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
-  Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})));
+  Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
+    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I);
 
 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
   {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, tactics= tactics});

--- a/src/Pure/Proof/extraction.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -384,7 +384,7 @@
 val add_expand_thms = fold add_expand_thm;
 
 val extraction_expand =
-  Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm));
+  Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
 
 
 (** types with computational content **)

--- a/src/Pure/Tools/codegen_data.ML	Sat Oct 07 07:41:56 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Mon Oct 09 02:19:49 2006 +0200
@@ -837,7 +837,7 @@
 local
   fun add_simple_attribute (name, f) =
     (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
-      (Context.map_theory o f);
+      (fn th => Context.mapping (f th) I);
 in
   val _ = map (Context.add_setup o add_simple_attribute) [
     ("func", add_func),