# HG changeset patch
# User wenzelm
# Date 1518977929 -3600
# Node ID 11716a084cae425836bfc77b4a249c706aa22775
# Parent  6dd41193a72aca99343b36a56a59ef3e00d4f56d
clarified signature;

diff -r 6dd41193a72a -r 11716a084cae src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -6,6 +6,8 @@
 
 signature ATTRIB =
 sig
+  type thms = Attrib.thms
+  type fact = Attrib.fact
   val print_attributes: bool -> Proof.context -> unit
   val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory
   val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory
@@ -28,14 +30,15 @@
   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
-  type thms = (thm list * Token.src list) list
-  val trim_context: thms -> thms
-  val global_notes: string -> (Attrib.binding * thms) list ->
-    theory -> (string * thm list) list * theory
-  val local_notes: string -> (Attrib.binding * thms) list ->
-    Proof.context -> (string * thm list) list * Proof.context
-  val generic_notes: string -> (Attrib.binding * thms) list ->
-    Context.generic -> (string * thm list) list * Context.generic
+  val trim_context_binding: Attrib.binding -> Attrib.binding
+  val trim_context_thms: thms -> thms
+  val trim_context_fact: fact -> fact
+  val global_notes: string -> fact list -> theory ->
+    (string * thm list) list * theory
+  val local_notes: string -> fact list -> Proof.context ->
+    (string * thm list) list * Proof.context
+  val generic_notes: string -> fact 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
   val setup: binding -> attribute context_parser -> string -> theory -> theory
@@ -49,9 +52,8 @@
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
-  val transform_facts: morphism -> (Attrib.binding * thms) list -> (Attrib.binding * thms) list
-  val partial_evaluation: Proof.context ->
-    (Attrib.binding * thms) list -> (Attrib.binding * thms) list
+  val transform_facts: morphism -> fact list -> fact list
+  val partial_evaluation: Proof.context -> fact list -> fact list
   val print_options: bool -> Proof.context -> unit
   val config_bool: binding -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int: binding -> (Context.generic -> int) -> int Config.T * (theory -> theory)
@@ -79,7 +81,7 @@
 structure Attrib: sig type binding = Attrib.binding include ATTRIB end =
 struct
 
-type binding = Attrib.binding;
+open Attrib;
 
 
 
@@ -180,9 +182,9 @@
 
 (* fact expressions *)
 
-type thms = (thm list * Token.src list) list;
-
-val trim_context: thms -> thms = (map o apfst o map) Thm.trim_context;
+val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src);
+val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context;
+fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms);
 
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
diff -r 6dd41193a72a -r 11716a084cae src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/bundle.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -57,7 +57,7 @@
 
 fun define_bundle (b, bundle) context =
   let
-    val bundle' = Attrib.trim_context bundle;
+    val bundle' = Attrib.trim_context_thms bundle;
     val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context);
     val context' = (Data.map o apfst o K) bundles' context;
   in (name, context') end;
@@ -71,7 +71,7 @@
   | NONE => error "Missing bundle target");
 
 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
-val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms;
 
 fun augment_target thms =
   Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
diff -r 6dd41193a72a -r 11716a084cae src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -20,9 +20,8 @@
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
   (*nested local theories primitives*)
-  val standard_facts: local_theory -> Proof.context ->
-    (Attrib.binding * Attrib.thms) list -> (Attrib.binding * Attrib.thms) list
-  val standard_notes: (int * int -> bool) -> string -> (Attrib.binding * Attrib.thms) list ->
+  val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list
+  val standard_notes: (int * int -> bool) -> string -> Attrib.fact list ->
     local_theory -> local_theory
   val standard_declaration: (int * int -> bool) ->
     (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
@@ -35,10 +34,8 @@
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes:
-    (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
+    (string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) ->
+    string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
   val abbrev: (Syntax.mode -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
     Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
@@ -46,8 +43,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 * Attrib.thms) list ->
-    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
+  val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list ->
+    local_theory -> local_theory
   val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
     local_theory -> local_theory
 
@@ -59,8 +56,8 @@
     local_theory -> local_theory
 
   (*locale target primitives*)
-  val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list ->
-    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
+  val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact 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 6dd41193a72a -r 11716a084cae src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -11,6 +11,7 @@
 struct
   type binding = binding * Token.src list;
   type thms = (thm list * Token.src list) list;
+  type fact = binding * thms;
 end;
 
 signature LOCAL_THEORY =
@@ -47,9 +48,8 @@
   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 * Attrib.thms) list -> local_theory ->
-    (string * thm list) list * local_theory
-  val notes_kind: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+  val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
+  val notes_kind: string -> Attrib.fact list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -87,8 +87,7 @@
 type operations =
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
-  notes: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
-    (string * thm list) list * local_theory,
+  notes: string -> Attrib.fact 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 6dd41193a72a -r 11716a084cae src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -40,7 +40,7 @@
     thm option * thm option -> thm list ->
     Element.context_i list ->
     declaration list ->
-    (string * (Attrib.binding * Attrib.thms) list) list ->
+    (string * Attrib.fact list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
@@ -55,8 +55,7 @@
   val specification_of: theory -> string -> term option * term list
 
   (* Storing results *)
-  val add_thmss: string -> string -> (Attrib.binding * Attrib.thms) list ->
-    Proof.context -> Proof.context
+  val add_thmss: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
@@ -141,7 +140,7 @@
   (*syntax declarations*)
   syntax_decls: (declaration * serial) list,
   (*theorem declarations*)
-  notes: ((string * (Attrib.binding * Attrib.thms) list) * serial) list,
+  notes: ((string * Attrib.fact list) * serial) list,
   (*locale dependencies (sublocale relation) in reverse order*)
   dependencies: ((string * (morphism * morphism)) * serial) list,
   (*mixin part of dependencies*)
@@ -592,21 +591,11 @@
 
 (* Theorems *)
 
-local
-
-val trim_fact = map Thm.trim_context;
-val trim_srcs = (map o map o Token.map_facts) (K trim_fact);
-
-fun trim_context_facts facts = facts |> map (fn ((b, atts), args) =>
-  ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args));
-
-in
-
 fun add_thmss loc kind facts ctxt =
   if null facts then ctxt
   else
     let
-      val stored_notes = ((kind, trim_context_facts facts), serial ());
+      val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ());
 
       fun global_notes morph thy = thy
         |> (snd o Attrib.global_notes kind
@@ -621,8 +610,6 @@
         ((change_locale loc o apfst o apsnd) (cons stored_notes) #> registrations)
     end;
 
-end;
-
 
 (* Declarations *)
 
diff -r 6dd41193a72a -r 11716a084cae src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/token.ML	Sun Feb 18 19:18:49 2018 +0100
@@ -70,6 +70,7 @@
   val get_name: T -> name_value option
   val declare_maxidx: T -> Proof.context -> Proof.context
   val map_facts: (string option -> thm list -> thm list) -> T -> T
+  val trim_context_src: src -> src
   val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> T
@@ -425,6 +426,8 @@
     | Fact (a, ths) => Fact (a, f a ths)
     | _ => v));
 
+val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
+
 
 (* transform *)