src/Pure/Syntax/printer.ML

   | mark_freevars (t as Var (xi, T)) =
       if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
       else Lexicon.const "_var" $ t
   | mark_freevars a = a;
 
-fun ast_of_term trf show_const_types no_freeTs show_types show_sorts tm =
+fun ast_of_term trf show_all_types no_freeTs 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 no_freeTs orelse t mem seen then (Lexicon.free x, seen)

       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
       | (c' as Const (c, T), ts) =>
-	if show_const_types
-	then Ast.mk_appl (constrain c' T) (map ast_of ts)
-	else trans c T ts
+          if show_all_types
+          then Ast.mk_appl (constrain c' T) (map ast_of ts)
+          else trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
     and trans a T args =
       ast_of (apply_trans "print translation" a (apply_typed show_sorts T (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)

     |> mark_freevars
     |> ast_of
   end;
 
 fun term_to_ast trf tm =
-  ast_of_term trf (! show_all_types) (! show_no_free_types) (! show_types orelse ! show_sorts orelse ! show_all_types)
-    (! show_sorts) tm;
+  ast_of_term trf (! show_all_types) (! show_no_free_types)
+    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
 
 
 
 (** type prtabs **)
 

                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
       in
         (case token_trans a args of     (*try token translation function*)
           Some s_len => [Pretty.raw_str s_len]
-        | None =>			(*try print translation functions*)
+        | None =>                       (*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
       end
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
       | astT (Ast.Variable x, _) = [Pretty.str x]