tuned;
authorwenzelm
Thu Aug 14 12:33:21 2014 +0200 (2014-08-14)
changeset 57938a9fa81e150c9
parent 57937 3bc4725b313e
child 57939 b3baeeabfe0b
tuned;
src/Pure/Isar/attrib.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 12:13:24 2014 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 12:33:21 2014 +0200
     1.3 @@ -138,11 +138,7 @@
     1.4      |> Local_Theory.background_theory_result (define_global binding att0 comment)
     1.5      |-> (fn name =>
     1.6        Local_Theory.map_contexts (K transfer_attributes)
     1.7 -      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
     1.8 -          let
     1.9 -            val naming = Name_Space.naming_of context;
    1.10 -            val binding' = Morphism.binding phi binding;
    1.11 -          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
    1.12 +      #> Local_Theory.generic_alias Attributes.map binding name
    1.13        #> pair name)
    1.14    end;
    1.15  
     2.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:13:24 2014 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:33:21 2014 +0200
     2.3 @@ -64,6 +64,9 @@
     2.4    val set_defsort: sort -> local_theory -> local_theory
     2.5    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     2.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     2.7 +  val generic_alias:
     2.8 +    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
     2.9 +    binding -> string -> local_theory -> local_theory
    2.10    val class_alias: binding -> class -> local_theory -> local_theory
    2.11    val type_alias: binding -> string -> local_theory -> local_theory
    2.12    val const_alias: binding -> string -> local_theory -> local_theory
    2.13 @@ -168,7 +171,7 @@
    2.14  
    2.15  fun mark_brittle lthy =
    2.16    if level lthy = 1 then
    2.17 -    map_top (fn (naming, operations, after_close, brittle, target) =>
    2.18 +    map_top (fn (naming, operations, after_close, _, target) =>
    2.19        (naming, operations, after_close, true, target)) lthy
    2.20    else lthy;
    2.21  
    2.22 @@ -258,12 +261,12 @@
    2.23  
    2.24  val operations_of = #operations o top_of;
    2.25  
    2.26 +fun operation f lthy = f (operations_of lthy) lthy;
    2.27 +fun operation2 f x y = operation (fn ops => f ops x y);
    2.28 +
    2.29  
    2.30  (* primitives *)
    2.31  
    2.32 -fun operation f lthy = f (operations_of lthy) lthy;
    2.33 -fun operation2 f x y = operation (fn ops => f ops x y);
    2.34 -
    2.35  val pretty = operation #pretty;
    2.36  val abbrev = operation2 #abbrev;
    2.37  val define = operation2 #define false;
    2.38 @@ -274,7 +277,7 @@
    2.39    assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
    2.40  
    2.41  
    2.42 -(* basic derived operations *)
    2.43 +(* theorems *)
    2.44  
    2.45  val notes = notes_kind "";
    2.46  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    2.47 @@ -293,6 +296,9 @@
    2.48            (Proof_Context.fact_alias binding' name)
    2.49        end));
    2.50  
    2.51 +
    2.52 +(* default sort *)
    2.53 +
    2.54  fun set_defsort S =
    2.55    declaration {syntax = true, pervasive = false}
    2.56      (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
    2.57 @@ -319,14 +325,21 @@
    2.58  
    2.59  (* name space aliases *)
    2.60  
    2.61 -fun alias global_alias local_alias b name =
    2.62 +fun generic_alias app b name =
    2.63 +  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    2.64 +    let
    2.65 +      val naming = Name_Space.naming_of context;
    2.66 +      val b' = Morphism.binding phi b;
    2.67 +    in app (Name_Space.alias_table naming b' name) context end);
    2.68 +
    2.69 +fun syntax_alias global_alias local_alias b name =
    2.70    declaration {syntax = true, pervasive = false} (fn phi =>
    2.71      let val b' = Morphism.binding phi b
    2.72      in Context.mapping (global_alias b' name) (local_alias b' name) end);
    2.73  
    2.74 -val class_alias = alias Sign.class_alias Proof_Context.class_alias;
    2.75 -val type_alias = alias Sign.type_alias Proof_Context.type_alias;
    2.76 -val const_alias = alias Sign.const_alias Proof_Context.const_alias;
    2.77 +val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
    2.78 +val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
    2.79 +val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
    2.80  
    2.81  
    2.82  
     3.1 --- a/src/Pure/Isar/method.ML	Thu Aug 14 12:13:24 2014 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 14 12:33:21 2014 +0200
     3.3 @@ -356,11 +356,7 @@
     3.4      |> Local_Theory.background_theory_result (define_global binding meth0 comment)
     3.5      |-> (fn name =>
     3.6        Local_Theory.map_contexts (K transfer_methods)
     3.7 -      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
     3.8 -          let
     3.9 -            val naming = Name_Space.naming_of context;
    3.10 -            val binding' = Morphism.binding phi binding;
    3.11 -          in Methods.map (Name_Space.alias_table naming binding' name) context end)
    3.12 +      #> Local_Theory.generic_alias Methods.map binding name
    3.13        #> pair name)
    3.14    end;
    3.15