tuned;

--- 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;

--- a/src/Pure/sign.ML	Fri Jan 13 01:13:03 2006 +0100
+++ b/src/Pure/sign.ML	Fri Jan 13 01:13:05 2006 +0100
@@ -724,7 +724,7 @@
       val syn' = Syntax.extend_consts [bclass] syn;
       val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
     in (naming, syn', tsig', consts) end)
-  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
+  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, NoSyn)];
 
 val add_classes = fold (gen_add_class intern_class);
 val add_classes_i = fold (gen_add_class (K I));