tuned signature;

--- a/src/Pure/Isar/element.ML	Thu Jun 11 10:03:54 2015 +0200
+++ b/src/Pure/Isar/element.ML	Thu Jun 11 10:44:04 2015 +0200
@@ -7,9 +7,10 @@
 
 signature ELEMENT =
 sig
+  type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list)
   datatype ('typ, 'term) stmt =
     Shows of (Attrib.binding * ('term * 'term list) list) list |
-    Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
+    Obtains of ('typ, 'term) obtain list
   type statement = (string, string) stmt
   type statement_i = (typ, term) stmt
   datatype ('typ, 'term, 'fact) ctxt =
@@ -61,9 +62,10 @@
 
 (* statement *)
 
+type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list);
 datatype ('typ, 'term) stmt =
   Shows of (Attrib.binding * ('term * 'term list) list) list |
-  Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
+  Obtains of ('typ, 'term) obtain list;
 
 type statement = (string, string) stmt;
 type statement_i = (typ, term) stmt;

--- a/src/Pure/Isar/obtain.ML	Thu Jun 11 10:03:54 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jun 11 10:44:04 2015 +0200
@@ -38,6 +38,7 @@
 
 signature OBTAIN =
 sig
+  val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
   val thatN: string
   val obtain: string -> (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
@@ -93,6 +94,16 @@
 
 
 
+(** specification elements **)
+
+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;
+
+
+
 (** obtain **)
 
 fun bind_judgment ctxt name =

--- a/src/Pure/Isar/specification.ML	Thu Jun 11 10:03:54 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Jun 11 10:44:04 2015 +0200
@@ -347,8 +347,6 @@
       in (([], prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
       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);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
             (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
@@ -377,8 +375,7 @@
             |>> (fn [(_, [th])] => th)
           end;
 
-        val more_atts = map (Attrib.internal o K)
-          [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
+        val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes obtains);
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = [((Binding.empty, []), [(thesis, [])])];