src/Pure/Syntax/printer.ML

       -> ast -> Pretty.T
   end
 end;
 
 functor PrinterFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
-  and SExtension: SEXTENSION sharing TypeExt.SynExt = SExtension.Parser.SynExt)
+  and SynTrans: SYN_TRANS sharing TypeExt.SynExt = SynTrans.Parser.SynExt)
   : PRINTER =
 struct
 
 structure Symtab = Symtab;
 structure SynExt = TypeExt.SynExt;
-open SExtension.Parser.Lexicon SynExt.Ast SynExt TypeExt SExtension;
+open SynTrans.Parser.Lexicon SynExt.Ast SynExt TypeExt SynTrans;
 
 
 (** options for printing **)
 
 val show_types = ref false;

 fun ast_of_term trf show_types show_sorts tm =
   let
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if t mem seen then (Free (x, dummyT), seen)
+          else if t mem seen then (free x, seen)
           else (t, t :: seen)
       | prune_typs (t as Var (xi, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if t mem seen then (Var (xi, dummyT), seen)
+          else if t mem seen then (var xi, seen)
           else (t, t :: seen)
       | prune_typs (t_seen as (Bound _, _)) = t_seen
       | prune_typs (Abs (x, ty, t), seen) =
           let val (t', seen') = prune_typs (t, seen);
           in (Abs (x, ty, t'), seen') end

             (t1' $ t2', seen'')
           end;
 
 
     fun ast_of (Const (a, _)) = trans a []
-      | ast_of (Free (x, ty)) = constrain x (Free (x, dummyT)) ty
-      | ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (Var (xi, dummyT)) ty
+      | ast_of (Free (x, ty)) = constrain x (free x) ty
+      | ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (var xi) ty
       | ast_of (Bound i) = Variable ("B." ^ string_of_int i)
       | ast_of (t as Abs _) = ast_of (abs_tr' t)
       | ast_of (t as _ $ _) =
           (case strip_comb t of
             (Const (a, _), args) => trans a args

       | None => raise Match)
           handle Match => mk_appl (Constant a) (map ast_of args)
 
     and constrain x t ty =
       if show_types andalso ty <> dummyT then
-        ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty)
+        ast_of (const constrainC $ t $ term_of_typ show_sorts ty)
       else Variable x;
   in
     if show_types then
       ast_of (#1 (prune_typs (prop_tr' show_sorts tm, [])))
     else ast_of (prop_tr' show_sorts tm)

 
 
 
 (** pretty term or typ asts **)
 
-fun chain[Block(_,pr)] = chain(pr)
-  | chain[Arg _] = true
+fun chain [Block (_, pr)] = chain pr
+  | chain [Arg _] = true
   | chain _  = false;
 
 fun pretty prtab trf type_mode ast0 p0 =
   let
     val trans = apply_trans "print ast translation";

       | synT (Break i :: symbs, args) =
           let val (Ts, args') = synT (symbs, args);
           in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
       | synT (_ :: _, []) = sys_error "synT"
 
-    and parT (pr, args, p, p': int) =
-          #1 (synT(if p > p' orelse
-                      (!show_brackets andalso p' <> max_pri andalso
-                       not(chain pr))
-                   then [Block (1, String "(" :: pr @ [String ")"])]
-                   else pr,
-                   args))
+    and parT (pr, args, p, p': int) = #1 (synT
+          (if p > p' orelse
+            (! show_brackets andalso p' <> max_pri andalso not (chain pr))
+            then [Block (1, String "(" :: pr @ [String ")"])]
+            else pr, args))
 
     and prefixT (_, a, [], _) = [Pretty.str a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
 
     and splitT 0 ([x], ys) = (x, ys)