equal
deleted
inserted
replaced
381 val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt)); |
381 val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt)); |
382 |
382 |
383 val shorten = |
383 val shorten = |
384 Name_Space.extern |
384 Name_Space.extern |
385 (ctxt |
385 (ctxt |
386 |> Config.put Name_Space.long_names false |
386 |> Config.put Name_Space.names_long false |
387 |> Config.put Name_Space.short_names false |
387 |> Config.put Name_Space.names_short false |
388 |> Config.put Name_Space.unique_names false) space; |
388 |> Config.put Name_Space.names_unique false) space; |
389 |
389 |
390 fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
390 fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
391 nicer_name (shorten x, i) (shorten y, j) |
391 nicer_name (shorten x, i) (shorten y, j) |
392 | nicer (Facts.Fact _) (Facts.Named _) = true |
392 | nicer (Facts.Fact _) (Facts.Named _) = true |
393 | nicer (Facts.Named _) (Facts.Fact _) = false; |
393 | nicer (Facts.Named _) (Facts.Fact _) = false; |