diff -r 00f4461fa99f -r 80ef19b51493 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Apr 18 15:51:48 2016 +0100
+++ b/src/Pure/Isar/obtain.ML	Mon Apr 18 20:24:19 2016 +0200
@@ -8,6 +8,7 @@
 sig
   val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context
   val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
+  val obtains_attribs: ('typ, 'term) Element.obtain list -> Token.src list
   val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
   val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
   val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
@@ -70,11 +71,15 @@
 
 (* result declaration *)
 
-fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) =
-  let
-    val case_names = obtains |> map_index (fn (i, (b, _)) =>
-      if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
-  in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end;
+fun case_names (obtains: ('typ, 'term) Element.obtain list) =
+  obtains |> map_index (fn (i, (b, _)) =>
+    if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
+
+fun obtains_attributes obtains =
+  [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names (case_names obtains)];
+
+fun obtains_attribs obtains =
+  [Attrib.consumes (~ (length obtains)), Attrib.case_names (case_names obtains)];
 
 
 (* obtain thesis *)