misc tuning and simplification;
authorwenzelm
Sat Mar 10 20:58:40 2012 +0100 (2012-03-10 ago)
changeset 4685979f712a9a815
parent 46858 05f30c796f95
child 46860 fe8d6532e1c1
misc tuning and simplification;
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 10 20:02:15 2012 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 10 20:58:40 2012 +0100
     1.3 @@ -99,12 +99,11 @@
     1.4       lists indexed by registration/dependency serial,
     1.5       entries for empty lists may be omitted *)
     1.6  
     1.7 -fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial');
     1.8 +fun lookup_mixins serial' mixins = Inttab.lookup_list mixins serial';
     1.9  
    1.10 -fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2);
    1.11 +fun merge_mixins mixs : mixins = Inttab.merge_list (eq_snd op =) mixs;
    1.12  
    1.13 -fun insert_mixin serial' mixin =
    1.14 -  Inttab.map_default (serial', []) (cons (mixin, serial ()));
    1.15 +fun insert_mixin serial' mixin = Inttab.cons_list (serial', (mixin, serial ()));
    1.16  
    1.17  fun rename_mixin (old, new) mix =
    1.18    (case Inttab.lookup mix old of
    1.19 @@ -465,8 +464,7 @@
    1.20      val activate =
    1.21        activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
    1.22    in
    1.23 -    roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
    1.24 -      dep (get_idents context, context)
    1.25 +    roundup thy activate (the_default Morphism.identity export) dep (get_idents context, context)
    1.26      |-> put_idents
    1.27    end;
    1.28  
    1.29 @@ -546,7 +544,7 @@
    1.30      val context' = Context.Theory thy';
    1.31      val (_, regs) =
    1.32        fold_rev (roundup thy' cons export)
    1.33 -        (registrations_of context' loc) (get_idents (context'), []);
    1.34 +        (registrations_of context' loc) (get_idents context', []);
    1.35    in
    1.36      thy'
    1.37      |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
    1.38 @@ -660,7 +658,7 @@
    1.39      val _ = the_locale thy name;  (* error if locale unknown *)
    1.40    in
    1.41      (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
    1.42 -      [] => Pretty.str ("no interpretations")
    1.43 +      [] => Pretty.str "no interpretations"
    1.44      | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
    1.45    end |> Pretty.writeln;
    1.46  
    1.47 @@ -670,7 +668,7 @@
    1.48      val idents = if clean then [] else get_idents (Context.Proof ctxt);
    1.49    in
    1.50      (case fold (roundup thy cons export) insts (idents, []) |> snd of
    1.51 -      [] => Pretty.str ("no dependencies")
    1.52 +      [] => Pretty.str "no dependencies"
    1.53      | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
    1.54    end |> Pretty.writeln;
    1.55