# HG changeset patch
# User wenzelm
# Date 1465466558 -7200
# Node ID ac1a0b81453e0485ced6278e7b769d69829efb5a
# Parent  3837a9ace1c7a36b371ae0e1a33c323be69988fe
tuned signature;

diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -33,11 +33,12 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
-  val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  type thms = (thm list * Token.src list) list
+  val global_notes: string -> (binding * thms) list ->
     theory -> (string * thm list) list * theory
-  val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  val local_notes: string -> (binding * thms) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  val generic_notes: string -> (binding * thms) list ->
     Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
   val attribute_syntax: attribute context_parser -> Token.src -> attribute
@@ -47,17 +48,13 @@
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
-  val internal_declaration: declaration -> (thm list * Token.src list) list
+  val internal_declaration: declaration -> thms
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
-  val transform_facts: morphism ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list
-  val partial_evaluation: Proof.context ->
-    (binding * (thm list * Token.src list) list) list ->
-    (binding * (thm list * Token.src list) list) list
+  val transform_facts: morphism -> (Attrib.binding * thms) list -> (Attrib.binding * thms) list
+  val partial_evaluation: Proof.context -> (binding * thms) list -> (binding * thms) list
   val print_options: bool -> Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -195,6 +192,8 @@
 
 (* fact expressions *)
 
+type thms = (thm list * Token.src list) list;
+
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
 
diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/bundle.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -6,11 +6,10 @@
 
 signature BUNDLE =
 sig
-  type bundle = (thm list * Token.src list) list
   val check: Proof.context -> xstring * Position.T -> string
-  val get_bundle: Proof.context -> string -> bundle
-  val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
-  val bundle: binding * (thm list * Token.src list) list ->
+  val get_bundle: Proof.context -> string -> Attrib.thms
+  val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms
+  val bundle: binding * Attrib.thms ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
@@ -32,14 +31,12 @@
 
 (* maintain bundles *)
 
-type bundle = (thm list * Token.src list) list;
-
-fun transform_bundle phi : bundle -> bundle =
+fun transform_bundle phi =
   map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
 
 structure Data = Generic_Data
 (
-  type T = bundle Name_Space.table;
+  type T = Attrib.thms Name_Space.table;
   val empty : T = Name_Space.empty_table "bundle";
   val extend = I;
   val merge = Name_Space.merge_tables;
diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -29,9 +29,9 @@
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes:
-    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
-      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
-    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
+    (string -> (Attrib.binding * Attrib.thms) list ->
+      (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory) ->
+    string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: (Syntax.mode -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
@@ -40,10 +40,8 @@
   (*theory target primitives*)
   val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
      term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_target_notes: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> local_theory
+  val theory_target_notes: string -> (Attrib.binding * Attrib.thms) list ->
+    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
   val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
     local_theory -> local_theory
 
@@ -55,10 +53,8 @@
     local_theory -> local_theory
 
   (*locale target primitives*)
-  val locale_target_notes: string -> string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> local_theory
+  val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list ->
+    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
   val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -10,6 +10,7 @@
 structure Attrib =
 struct
   type binding = binding * Token.src list;
+  type thms = (thm list * Token.src list) list;
 end;
 
 signature LOCAL_THEORY =
@@ -45,10 +46,10 @@
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
-  val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
-  val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
+  val notes: (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory
+  val notes_kind: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
@@ -85,9 +86,8 @@
 type operations =
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
-  notes: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory,
+  notes: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -35,7 +35,7 @@
     thm option * thm option -> thm list ->
     Element.context_i list ->
     declaration list ->
-    (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
+    (string * (Attrib.binding * Attrib.thms) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
@@ -50,7 +50,7 @@
   val specification_of: theory -> string -> term option * term list
 
   (* Storing results *)
-  val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
+  val add_thmss: string -> string -> (Attrib.binding * Attrib.thms) list ->
     Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
@@ -135,7 +135,7 @@
   (*syntax declarations*)
   syntax_decls: (declaration * serial) list,
   (*theorem declarations*)
-  notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
+  notes: ((string * (Attrib.binding * Attrib.thms) list) * serial) list,
   (*locale dependencies (sublocale relation) in reverse order*)
   dependencies: ((string * (morphism * morphism)) * serial) list,
   (*mixin part of dependencies*)
diff -r 3837a9ace1c7 -r ac1a0b81453e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Jun 09 12:02:38 2016 +0200
@@ -51,7 +51,7 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * Attrib.thms) list ->
     (binding * typ option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->