# HG changeset patch
# User wenzelm
# Date 1518979741 -3600
# Node ID 49f45fcd335b7a8ee9491745c21830659921e914
# Parent  4ba01fea9cfd852639d7ce4fc03e27e88290d841
clarified signature;

diff -r 4ba01fea9cfd -r 49f45fcd335b src/Pure/Isar/generic_target.ML
--- 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
diff -r 4ba01fea9cfd -r 49f45fcd335b src/Pure/Isar/locale.ML
--- 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 ***)