# HG changeset patch # User wenzelm # Date 1138727968 -3600 # Node ID 11c92ec2c29c882710ae8b2b17bc6d711c0edf75 # Parent 020044cf15100517bae2acf638d06686fc3681e8 tuned LocalTheory.pretty_consts; diff -r 020044cf1510 -r 11c92ec2c29c src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Tue Jan 31 18:19:27 2006 +0100 +++ b/src/Pure/Isar/constdefs.ML Tue Jan 31 18:19:28 2006 +0100 @@ -63,7 +63,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 decls); thy' end; + in Pretty.writeln (LocalTheory.pretty_consts ctxt (K true) decls); thy' end; val add_constdefs = gen_constdefs ProofContext.read_vars_legacy ProofContext.read_term_legacy Attrib.attribute;