# HG changeset patch
# User wenzelm
# Date 1236782172 -3600
# Node ID ce5138c92ca74bc917251dfa55be4aceabd9abd3
# Parent  aad3cd70e25a2f5f298ad004c6425da76735271e
added def_binding_optional -- robust version of def_name_optional for bindings;

diff -r aad3cd70e25a -r ce5138c92ca7 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/Pure/more_thm.ML	Wed Mar 11 15:36:12 2009 +0100
@@ -57,6 +57,7 @@
   val default_position_of: thm -> thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
+  val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
@@ -353,6 +354,9 @@
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
+fun def_binding_optional b name =
+  if Binding.is_empty name then Binding.map_name def_name b else name;
+
 
 (* unofficial theorem names *)