# 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;