equal
deleted
inserted
replaced
912 step :: aux subst depth nextp proof |
912 step :: aux subst depth nextp proof |
913 in aux [] 0 (1, 1) end |
913 in aux [] 0 (1, 1) end |
914 |
914 |
915 fun string_for_proof ctxt i n = |
915 fun string_for_proof ctxt i n = |
916 let |
916 let |
917 fun fix_print_mode f = |
917 fun fix_print_mode f x = |
918 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
918 setmp_CRITICAL show_no_free_types true |
919 (print_mode_value ())) f |
919 (setmp_CRITICAL show_types true |
|
920 (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
|
921 (print_mode_value ())) f)) x |
920 fun do_indent ind = replicate_string (ind * indent_size) " " |
922 fun do_indent ind = replicate_string (ind * indent_size) " " |
921 fun do_free (s, T) = |
923 fun do_free (s, T) = |
922 maybe_quote s ^ " :: " ^ |
924 maybe_quote s ^ " :: " ^ |
923 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) |
925 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) |
924 fun do_label l = if l = no_label then "" else string_for_label l ^ ": " |
926 fun do_label l = if l = no_label then "" else string_for_label l ^ ": " |