# HG changeset patch
# User wenzelm
# Date 1138465737 -3600
# Node ID 916c493b7f0ca7729a389834fac30efe67afe998
# Parent  9dc194c479aade40bd36c088e37bfba5002400da
added print_consts;
tuned;

diff -r 9dc194c479aa -r 916c493b7f0c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jan 28 17:28:56 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Jan 28 17:28:57 2006 +0100
@@ -11,25 +11,26 @@
   val hyps_of: Proof.context -> term list
   val standard: Proof.context -> thm -> thm
   val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T
+  val print_consts: Proof.context -> (string * typ) list -> unit
   val theory: (theory -> theory) -> Proof.context -> Proof.context
   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val init: xstring option -> theory -> Proof.context
   val init_i: string option -> theory -> Proof.context
   val exit: Proof.context -> Proof.context * theory
-  val consts: ((string * typ) * mixfix) list -> Proof.context -> term list * Proof.context
-  val axioms: ((string * Attrib.src list) * term list) list -> Proof.context ->
+  val consts: ((bstring * typ) * mixfix) list -> Proof.context -> term list * Proof.context
+  val axioms: ((bstring * Attrib.src list) * term list) list -> Proof.context ->
     (bstring * thm list) list * Proof.context
   val axioms_finish: (Proof.context -> thm -> thm) ->
-    ((string * Attrib.src list) * term list) list -> Proof.context ->
+    ((bstring * Attrib.src list) * term list) list -> Proof.context ->
     (bstring * thm list) list * Proof.context
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     Proof.context -> (bstring * thm list) list * Proof.context
   val note: (bstring * Attrib.src list) * thm list -> Proof.context ->
     (bstring * thm list) * Proof.context
-  val def: (string * mixfix) * ((string * Attrib.src list) * term) ->
+  val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     Proof.context -> (term * (bstring * thm)) * Proof.context
   val def_finish: (Proof.context -> term -> thm -> thm) ->
-    (string * mixfix) * ((string * Attrib.src list) * term) ->
+    (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     Proof.context -> (term * (bstring * thm)) * Proof.context
 end;
 
@@ -66,7 +67,7 @@
   | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt);
 
 
-(* pretty_consts *)
+(* print consts *)
 
 local
 
@@ -83,6 +84,9 @@
     [] => pretty_vars ctxt "constants" cs
   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
 
+fun print_consts _ [] = ()
+  | print_consts ctxt cs = Pretty.writeln (pretty_consts ctxt cs);
+
 end;