--- 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