summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 02 Jun 2010 14:35:52 +0200 | |

changeset 37319 | 42268dc7d6c4 |

parent 37318 | 32b3d16b04f6 |

child 37320 | 06c7a2f231fe |

show types in Isar proofs, but not for free variables;
this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 02 12:28:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 02 14:35:52 2010 +0200 @@ -914,9 +914,11 @@ fun string_for_proof ctxt i n = let - fun fix_print_mode f = - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) f + fun fix_print_mode f x = + setmp_CRITICAL show_no_free_types true + (setmp_CRITICAL show_types true + (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) f)) x fun do_indent ind = replicate_string (ind * indent_size) " " fun do_free (s, T) = maybe_quote s ^ " :: " ^