tuned;
authorwenzelm
Sat Mar 10 20:02:15 2012 +0100 (2012-03-10)
changeset 4685805f30c796f95
parent 46857 628b4a3fbf6e
child 46859 79f712a9a815
tuned;
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Tools/interpretation_with_defs.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 10 19:49:32 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 10 20:02:15 2012 +0100
     1.3 @@ -814,17 +814,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun note_eqns_register deps witss attrss eqns export export' context =
     1.8 -  context
     1.9 -  |> Element.generic_note_thmss Thm.lemmaK
    1.10 +fun note_eqns_register deps witss attrss eqns export export' =
    1.11 +  Element.generic_note_thmss Thm.lemmaK
    1.12      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.13 -  |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.14 -  |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.15 +  #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.16 +  #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.17      fn context =>
    1.18 -      Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.19 -          (map (Element.transform_witness export') wits))
    1.20 -        (Element.eq_morphism (Context.theory_of context) eqns |>
    1.21 -          Option.map (rpair true))
    1.22 +      Locale.add_registration
    1.23 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.24 +        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
    1.25          export context) (deps ~~ witss));
    1.26  
    1.27  fun gen_interpretation prep_expr parse_prop prep_attr
     2.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 10 19:49:32 2012 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 10 20:02:15 2012 +0100
     2.3 @@ -107,9 +107,9 @@
     2.4    Inttab.map_default (serial', []) (cons (mixin, serial ()));
     2.5  
     2.6  fun rename_mixin (old, new) mix =
     2.7 -  case Inttab.lookup mix old of
     2.8 -    NONE => mix |
     2.9 -    SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
    2.10 +  (case Inttab.lookup mix old of
    2.11 +    NONE => mix
    2.12 +  | SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs));
    2.13  
    2.14  fun compose_mixins mixins =
    2.15    fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    2.16 @@ -391,7 +391,8 @@
    2.17      |> compose_mixins
    2.18    end;
    2.19  
    2.20 -fun get_registrations context select = Registrations.get context
    2.21 +fun get_registrations context select =
    2.22 +  Registrations.get context
    2.23    |>> Idtab.dest |>> select
    2.24    (* with inherited mixins *)
    2.25    |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
    2.26 @@ -543,8 +544,9 @@
    2.27          (apfst (cons ((name, (morph, export)), serial')) #>
    2.28            apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
    2.29      val context' = Context.Theory thy';
    2.30 -    val (_, regs) = fold_rev (roundup thy' cons export)
    2.31 -      (registrations_of context' loc) (get_idents (context'), []);
    2.32 +    val (_, regs) =
    2.33 +      fold_rev (roundup thy' cons export)
    2.34 +        (registrations_of context' loc) (get_idents (context'), []);
    2.35    in
    2.36      thy'
    2.37      |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
    2.38 @@ -674,7 +676,7 @@
    2.39  
    2.40  fun locale_deps thy =
    2.41    let
    2.42 -    val names = all_locales thy
    2.43 +    val names = all_locales thy;
    2.44      fun add_locale_node name =
    2.45        let
    2.46          val params = params_of thy name;
    2.47 @@ -690,7 +692,8 @@
    2.48          val dependencies =
    2.49            map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
    2.50        in
    2.51 -        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
    2.52 +        fold (fn (super, ts) => fn (gr, deps) =>
    2.53 +         (gr |> Graph.add_edge (super, name),
    2.54            deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
    2.55              dependencies
    2.56        end;
     3.1 --- a/src/Tools/interpretation_with_defs.ML	Sat Mar 10 19:49:32 2012 +0100
     3.2 +++ b/src/Tools/interpretation_with_defs.ML	Sat Mar 10 20:02:15 2012 +0100
     3.3 @@ -17,20 +17,19 @@
     3.4  structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
     3.5  struct
     3.6  
     3.7 -fun note_eqns_register deps witss def_eqns attrss eqns export export' context =
     3.8 +fun note_eqns_register deps witss def_eqns attrss eqns export export' =
     3.9    let
    3.10      fun meta_rewrite context =
    3.11        map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
    3.12          maps snd;
    3.13    in
    3.14 -    context
    3.15 -    |> Element.generic_note_thmss Thm.lemmaK
    3.16 +    Element.generic_note_thmss Thm.lemmaK
    3.17        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    3.18 -    |-> (fn facts => `(fn context => meta_rewrite context facts))
    3.19 -    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    3.20 +    #-> (fn facts => `(fn context => meta_rewrite context facts))
    3.21 +    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    3.22        fn context =>
    3.23 -        Locale.add_registration (dep, morph $> Element.satisfy_morphism
    3.24 -            (map (Element.transform_witness export') wits))
    3.25 +        Locale.add_registration
    3.26 +          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    3.27            (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
    3.28              Option.map (rpair true))
    3.29            export context) (deps ~~ witss))