--- 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);
--- 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;
--- 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
--- 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,
--- 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*)
--- 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 ->