# HG changeset patch
# User berghofe
# Date 1076517501 -3600
# Node ID 09aab47107895b24ac314d52e14d5ad4161f2df0
# Parent  9fb68cd747193524879e8064986b6f424e884930
Printing functions now use cond_extrn instead of extrn
(due to short_names flag)

diff -r 9fb68cd74719 -r 09aab4710789 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Feb 11 17:36:08 2004 +0100
+++ b/src/Pure/sign.ML	Wed Feb 11 17:38:21 2004 +0100
@@ -487,15 +487,15 @@
   val spaces_of = #spaces o rep_sg;
 in
   fun intrn_class spaces = intrn spaces classK;
-  fun extrn_class spaces = extrn spaces classK;
+  fun extrn_class spaces = cond_extrn spaces classK;
 
   val intrn_sort = map o intrn_class;
   val intrn_typ = trn_typ o intrn;
   val intrn_term = trn_term o intrn;
 
   val extrn_sort = map o extrn_class;
-  val extrn_typ = trn_typ o extrn;
-  val extrn_term = trn_term o extrn;
+  val extrn_typ = trn_typ o cond_extrn;
+  val extrn_term = trn_term o cond_extrn;
 
   fun intrn_tycons spaces T =
     map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;