src/Pure/Isar/proof.ML

   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
   val fix: (Name.binding * string option * mixfix) list -> state -> state
   val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
   val assm: Assumption.export ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
+    (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
     ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
-  val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    state -> state
+  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
     state -> state
-  val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    state -> state
+  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
     state -> state
-  val def: ((Name.binding * Attrib.src list) *
-    ((Name.binding * mixfix) * (string * string list))) list -> state -> state
+  val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
+    state -> state
   val def_i: ((Name.binding * attribute list) *
     ((Name.binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
-  val note_thmss: ((Name.binding * Attrib.src list) *
-    (Facts.ref * Attrib.src list) list) list -> state -> state
+  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   val note_thmss_i: ((Name.binding * attribute list) *
     (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state

   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
   val global_done_proof: state -> context
   val global_skip_proof: bool -> state -> context
   val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
 end;
 
 structure Proof: PROOF =