# HG changeset patch
# User wenzelm
# Date 878726539 -3600
# Node ID e57d03a5fc73821d9266431f340dc194f26aa570
# Parent  00136226f74b2b310e31d787eab1ec115bbc280d
print translation: added show_sorts argument;

diff -r 00136226f74b -r e57d03a5fc73 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Nov 05 11:41:46 1997 +0100
+++ b/src/Pure/Syntax/printer.ML	Wed Nov 05 11:42:19 1997 +0100
@@ -17,9 +17,12 @@
 signature PRINTER =
 sig
   include PRINTER0
-  val term_to_ast: (string -> (typ -> term list -> term) option) -> term -> Ast.ast
-  val typ_to_ast: (string -> (typ -> term list -> term) option) -> typ -> Ast.ast
-  val sort_to_ast: (string -> (typ -> term list -> term) option) -> sort -> Ast.ast
+  val term_to_ast: (string -> (bool -> typ -> term list -> term) option)
+    -> term -> Ast.ast
+  val typ_to_ast: (string -> (bool -> typ -> term list -> term) option)
+    -> typ -> Ast.ast
+  val sort_to_ast: (string -> (bool -> typ -> term list -> term) option)
+    -> sort -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
@@ -57,6 +60,8 @@
     Match => raise Match
   | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
 
+fun uncurry3 f (x, y, z) = f x y z;
+
 
 (* simple_ast_of *)
 
@@ -87,7 +92,8 @@
       | ast_of t = raise TERM ("ast_of_termT: bad term encoding of type", [t])
     and trans a args =
       (case trf a of
-        Some f => ast_of (apply_trans "print translation" a (uncurry f) (dummyT, args))
+        Some f => ast_of (apply_trans "print translation" a (uncurry3 f)
+          (false, dummyT, args))
       | None => raise Match)
           handle Match => mk_appl (Constant a) (map ast_of args);
   in
@@ -144,7 +150,9 @@
 
     and trans a T args =
       (case trf a of
-        Some f => ast_of (apply_trans "print translation" a (uncurry f) (T, args))
+        Some f =>
+          ast_of (apply_trans "print translation" a (uncurry3 f)
+            (show_sorts, T, args))
       | None => raise Match)
           handle Match => mk_appl (Constant a) (map ast_of args)
 
@@ -155,7 +163,7 @@
       else simple_ast_of t
   in
     tm
-    |> prop_tr' show_sorts
+    |> prop_tr'
     |> (if show_types then #1 o prune_typs o rpair [] else I)
     |> mark_freevars
     |> ast_of