tuned;
authorwenzelm
Fri Jan 13 01:13:05 2006 +0100 (2006-01-13)
changeset 1866785d04c28224a
parent 18666 f37a43cec547
child 18668 4a15c09bd46a
tuned;
src/Pure/Isar/context_rules.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Fri Jan 13 01:13:03 2006 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Jan 13 01:13:05 2006 +0100
     1.3 @@ -163,9 +163,9 @@
     1.4  
     1.5  (* wrappers *)
     1.6  
     1.7 -fun gen_add_wrapper upd w = Context.the_theory o
     1.8 -  Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
     1.9 -    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)) o Context.Theory;
    1.10 +fun gen_add_wrapper upd w =
    1.11 +  Context.map_theory (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.12 +    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
    1.13  
    1.14  val addSWrapper = gen_add_wrapper Library.apfst;
    1.15  val addWrapper = gen_add_wrapper Library.apsnd;
     2.1 --- a/src/Pure/sign.ML	Fri Jan 13 01:13:03 2006 +0100
     2.2 +++ b/src/Pure/sign.ML	Fri Jan 13 01:13:05 2006 +0100
     2.3 @@ -724,7 +724,7 @@
     2.4        val syn' = Syntax.extend_consts [bclass] syn;
     2.5        val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
     2.6      in (naming, syn', tsig', consts) end)
     2.7 -  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
     2.8 +  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, NoSyn)];
     2.9  
    2.10  val add_classes = fold (gen_add_class intern_class);
    2.11  val add_classes_i = fold (gen_add_class (K I));