# HG changeset patch
# User wenzelm
# Date 1160177473 -7200
# Node ID e0223c1bd7e8bb7a8104ca4d9e1cafc2b80ef593
# Parent  e57588ae75002d45c25f6058bf3d7d3ef1edf696
Thm.def_name_optional;
ProofDisplay.pretty_consts;

diff -r e57588ae7500 -r e0223c1bd7e8 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat Oct 07 01:31:12 2006 +0200
+++ b/src/Pure/Isar/constdefs.ML	Sat Oct 07 01:31:13 2006 +0200
@@ -44,7 +44,7 @@
       else ());
 
     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
-    val name = if raw_name = "" then Thm.def_name c else raw_name;
+    val name = Thm.def_name_optional c raw_name;
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
@@ -58,7 +58,7 @@
     val ctxt = ProofContext.init thy;
     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
     val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
-  in Pretty.writeln (LocalTheory.pretty_consts ctxt (K true) decls); thy' end;
+  in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
   ProofContext.read_term_legacy Attrib.attribute;