# HG changeset patch # User wenzelm # Date 780597323 -3600 # Node ID 94436ad4b60d53f1bbd4d4c56a7b944e3d3f2ef7 # Parent 2b1e384fae33e922eeca9bbf60c7eee301a888f1 added flag show_no_free_types: bool ref; diff -r 2b1e384fae33 -r 94436ad4b60d src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Mon Sep 26 17:34:59 1994 +0100 +++ b/src/Pure/Syntax/printer.ML Mon Sep 26 17:35:23 1994 +0100 @@ -10,6 +10,7 @@ val show_brackets: bool ref val show_sorts: bool ref val show_types: bool ref + val show_no_free_types: bool ref end; signature PRINTER = @@ -46,6 +47,8 @@ val show_types = ref false; val show_sorts = ref false; val show_brackets = ref false; +val show_no_free_types = ref false; + (** convert term or typ to ast **) @@ -58,14 +61,16 @@ fun ast_of_term trf show_types show_sorts tm = let + val no_freeTs = ! show_no_free_types; + 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, seen) + else if no_freeTs orelse 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, seen) + else if no_freeTs orelse 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) =