src/Pure/more_thm.ML

   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   type attribute = Context.generic * thm -> Context.generic option * thm option
   type binding = binding * attribute list
-  val empty_binding: binding
   val tag_rule: string * string -> thm -> thm
   val untag_rule: string -> thm -> thm
   val is_free_dummy: thm -> bool
   val tag_free_dummy: thm -> thm
   val def_name: string -> string

 
 (*attributes subsume any kind of rules or context modifiers*)
 type attribute = Context.generic * thm -> Context.generic option * thm option;
 
 type binding = binding * attribute list;
-val empty_binding: binding = (Binding.empty, []);
 
 fun rule_attribute ths f (x, th) =
   (NONE,
     (case find_first is_free_dummy (th :: ths) of
       SOME th' => SOME th'