src/Pure/Isar/proof.ML

   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
   val match_bind: (string list * string) list -> state -> state
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
-  val fix: (string * string option * mixfix) list -> state -> state
-  val fix_i: (string * typ option * mixfix) 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 ->
-    ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+    ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
-    ((string * attribute list) * (term * term list) list) list -> state -> state
-  val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
-  val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
-  val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
-  val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
-  val def: ((string * Attrib.src list) *
-    ((string * mixfix) * (string * string list))) list -> state -> state
-  val def_i: ((string * attribute list) *
-    ((string * mixfix) * (term * term list))) list -> state -> state
+    ((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_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_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_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: ((string * Attrib.src list) *
+  val note_thmss: ((Name.binding * Attrib.src list) *
     (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: ((string * attribute list) *
+  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 with_thmss_i: ((thm list * attribute list) list) list -> state -> state

   val apply_end: Method.text -> state -> state Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
     string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * 'a list) * 'b) list -> state -> state
+    ((Name.binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state Seq.seq
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
   val theorem_i: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> 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) ->
-    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
+    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
+    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
 end;
 
 structure Proof: PROOF =
 struct
 

   #> chain;
 
 
 (* note etc. *)
 
-fun no_binding args = map (pair ("", [])) args;
+fun no_binding args = map (pair (Name.no_binding, [])) args;
 
 local
 
 fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
   state

 val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
 
 val local_results =
   gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
 
-fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
+fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
 
 end;
 
 
 (* using/unfolding *)

 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   let
     val atts = map (prep_att (theory_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
-    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
+    val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
   in
     state'
     |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
     |> assume_i assumptions
     |> add_binds_i AutoBind.no_facts
     |> map_context (ProofContext.restore_naming (context_of state))
-    |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
+    |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
   end;
 
 in
 
 val invoke_case = gen_invoke_case Attrib.attribute;