--- a/src/Pure/Isar/generic_target.ML Sun Feb 18 19:41:25 2018 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Feb 18 19:49:01 2018 +0100
@@ -383,7 +383,7 @@
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
(fn lthy => lthy |>
Local_Theory.target (fn ctxt => ctxt |>
- Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
+ Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #>
standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
fun locale_target_declaration locale syntax decl lthy = lthy
--- a/src/Pure/Isar/locale.ML Sun Feb 18 19:41:25 2018 +0100
+++ b/src/Pure/Isar/locale.ML Sun Feb 18 19:49:01 2018 +0100
@@ -55,7 +55,7 @@
val specification_of: theory -> string -> term option * term list
(* Storing results *)
- val add_thmss: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
+ val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
(* Activation *)
@@ -585,7 +585,7 @@
(* Theorems *)
-fun add_thmss loc kind facts ctxt =
+fun add_facts loc kind facts ctxt =
if null facts then ctxt
else
let
@@ -609,7 +609,7 @@
fun add_declaration loc syntax decl =
syntax ?
Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_thmss loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
+ #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
(*** Reasoning about locales ***)