src/Pure/Isar/obtain.ML

 
 signature OBTAIN =
 sig
   val thatN: string
   val obtain: string -> (binding * string option * mixfix) list ->
-    (Attrib.binding * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_i: string -> (binding * typ option * mixfix) list ->
-    ((binding * attribute list) * (term * term list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     (cterm list * thm list) * Proof.context
   val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;

     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
-    val xs = map (Binding.base_name o #1) vars;
+    val xs = map (Binding.name_of o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;

         Proof.fix_i vars
         #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
       [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
+    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
 in
 

     val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
   in ((vars', rule''), ctxt') end;
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Binding.base_name binding;
+    val x = Binding.name_of binding;
     val (T, ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =
   let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))

       in
         state'
         |> Proof.map_context (K ctxt')
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
-          (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
+          (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
         |> Proof.add_binds_i AutoBind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =

     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
-      "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
+      "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
     |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   end;
 
 in