# HG changeset patch
# User wenzelm
# Date 1465467675 -7200
# Node ID 27d51aa2d7119bb019ada7bd62e449c8bf9eeb08
# Parent  df955dd2dc092503806a42959f971dabf05e0eb6
tuned signature;

diff -r df955dd2dc09 -r 27d51aa2d711 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Jun 09 12:16:52 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Jun 09 12:21:15 2016 +0200
@@ -20,6 +20,12 @@
   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 ->
+    local_theory -> local_theory
+  val standard_declaration: (int * int -> bool) ->
+    (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory