# HG changeset patch
# User wenzelm
# Date 1160177472 -7200
# Node ID e57588ae75002d45c25f6058bf3d7d3ef1edf696
# Parent  b432f20a47ca418c8f4f941f43a3fe5c6d01f554
added def_name_optional;

diff -r b432f20a47ca -r e57588ae7500 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Oct 07 01:31:11 2006 +0200
+++ b/src/Pure/thm.ML	Sat Oct 07 01:31:12 2006 +0200
@@ -90,6 +90,7 @@
   val get_axiom_i: theory -> string -> thm
   val get_axiom: theory -> xstring -> thm
   val def_name: string -> string
+  val def_name_optional: string -> string -> string
   val get_def: theory -> xstring -> thm
   val axioms_of: theory -> (string * thm) list
 
@@ -594,7 +595,11 @@
 fun get_axiom thy =
   get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy);
 
-fun def_name name = name ^ "_def";
+fun def_name c = c ^ "_def";
+
+fun def_name_optional c "" = def_name c
+  | def_name_optional _ name = name;
+
 fun get_def thy = get_axiom thy o def_name;