# HG changeset patch
# User wenzelm
# Date 1136918017 -3600
# Node ID e135f6a1b76c5aaf41543a5bc936e88eb8e0655e
# Parent  33a6f6caa6172beb78d062bf3e5c3c94b792e2a0
Specification.pretty_consts ctxt;

diff -r 33a6f6caa617 -r e135f6a1b76c src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Jan 10 19:33:36 2006 +0100
+++ b/src/Pure/Isar/constdefs.ML	Tue Jan 10 19:33:37 2006 +0100
@@ -65,9 +65,10 @@
 
 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
   let
-    val structs = #1 (fold_map prep_vars raw_structs (ProofContext.init thy));
+    val ctxt = ProofContext.init thy;
+    val structs = #1 (fold_map prep_vars raw_structs ctxt);
     val (decls, thy') = fold_map (gen_constdef prep_typ prep_term prep_att structs) specs thy
-  in Pretty.writeln (Specification.pretty_consts thy' decls); thy' end;
+  in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal
   ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;