src/Pure/Isar/attrib.ML
changeset 45584 41a768a431a6
parent 45537 8e3e004f1c31
child 45586 c94f149cdf5d
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Nov 19 12:33:18 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Nov 19 13:02:50 2011 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    type src = Args.src
     1.5    type binding = binding * src list
     1.6    val empty_binding: binding
     1.7 +  val is_empty_binding: binding -> bool
     1.8    val print_attributes: theory -> unit
     1.9    val intern: theory -> xstring -> string
    1.10    val intern_src: theory -> src -> src
    1.11 @@ -60,7 +61,9 @@
    1.12  type src = Args.src;
    1.13  
    1.14  type binding = binding * src list;
    1.15 +
    1.16  val empty_binding: binding = (Binding.empty, []);
    1.17 +fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
    1.18  
    1.19  
    1.20