src/Pure/Isar/context_rules.ML
changeset 18667 85d04c28224a
parent 18637 33a6f6caa617
child 18692 2270e25e9128
--- a/src/Pure/Isar/context_rules.ML	Fri Jan 13 01:13:03 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Jan 13 01:13:05 2006 +0100
@@ -163,9 +163,9 @@
 
 (* wrappers *)
 
-fun gen_add_wrapper upd w = Context.the_theory o
-  Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
-    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)) o Context.Theory;
+fun gen_add_wrapper upd w =
+  Context.map_theory (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
 
 val addSWrapper = gen_add_wrapper Library.apfst;
 val addWrapper = gen_add_wrapper Library.apsnd;