# HG changeset patch
# User wenzelm
# Date 1136672875 -3600
# Node ID 2f3c24533aea59bb344f8ecffde560c85089c7f9
# Parent  3618d5ae0ac8023c0081b886643f7940ffe6b2ae
Specification.pretty_consts;

diff -r 3618d5ae0ac8 -r 2f3c24533aea src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat Jan 07 23:27:53 2006 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Jan 07 23:27:55 2006 +0100
@@ -24,13 +24,6 @@
 
 (** add_constdefs(_i) **)
 
-fun pretty_const thy (c, T) =
-  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
-    Pretty.quote (Sign.pretty_typ thy T)];
-
-fun pretty_constdefs thy decls =
-  Pretty.big_list "constants" (map (pretty_const thy) decls);
-
 fun gen_constdef prep_typ prep_term prep_att
     structs (decl, ((raw_name, raw_atts), raw_prop)) thy =
   let
@@ -74,7 +67,7 @@
   let
     val structs = #1 (fold_map prep_vars raw_structs (ProofContext.init thy));
     val (decls, thy') = fold_map (gen_constdef prep_typ prep_term prep_att structs) specs thy
-  in Pretty.writeln (pretty_constdefs thy' decls); thy' end;
+  in Pretty.writeln (Specification.pretty_consts thy' decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal
   ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;