| changeset 9274 | 21c302a2fd9a |
| parent 9196 | 1f6f66fe777a |
| child 9291 | 23705d14be8f |
--- a/src/Pure/Isar/proof_context.ML Thu Jul 06 18:11:48 2000 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Jul 06 18:12:17 2000 +0200 @@ -175,7 +175,7 @@ (* local theorems *) fun pretty_thms (Context {thms, ...}) = - pretty_items pretty_thm "local theorems:" (mapfilter smash_option (Symtab.dest thms)); + pretty_items pretty_thm "facts:" (mapfilter smash_option (Symtab.dest thms)); val print_thms = Pretty.writeln o Pretty.chunks o pretty_thms;