src/Pure/Isar/proof.ML

   #> chain;
 
 
 (* note etc. *)
 
-fun no_binding args = map (pair (Binding.empty, [])) args;
+fun empty_bindings args = map (pair Binding.empty_atts) args;
 
 local
 
 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   state

 in
 
 val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
 val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
 
-val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings;
 val from_thmss_cmd =
-  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
-
-val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
+
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings;
 val with_thmss_cmd =
-  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
+  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
 end;
 

 fun gen_using f g prep_att prep_fact args state =
   state
   |> assert_backward
   |> map_context_result
     (fn ctxt => ctxt |> Proof_Context.note_thmss ""
-      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
+      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (empty_bindings args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) =>
       let
         val ctxt = context_of state';
         val ths = maps snd named_facts;

     val (decls, fixes) = chop (length raw_decls) vars;
     val show_term = Syntax.string_of_term vars_ctxt;
 
     (*defs*)
     fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
-          if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+          if x = y then ((b, mx), (Binding.empty_atts, t)) :: match_defs more_decls more_defs
           else
             error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
               show_term (Free (y, U)))
       | match_defs [] [] = []
       | match_defs more_decls more_defs =