# HG changeset patch
# User wenzelm
# Date 1408010109 -7200
# Node ID 74ea9ba645c3bb27b9d40367e100b07856d269f3
# Parent  c578f3a37a67fc7b4bc576b243b0a32d70295563
tuned signature;

diff -r c578f3a37a67 -r 74ea9ba645c3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:51:17 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:09 2014 +0200
@@ -38,6 +38,7 @@
   val generic_notes: string -> (binding * (thm list * src list) list) list ->
     Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
+  val attribute_syntax: attribute context_parser -> Args.src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory