| changeset 62821 | 48c24d0b6d85 |
| parent 62819 | d3ff367a16a0 |
| child 62878 | 1cec457e0a03 |
--- a/src/Pure/Isar/runtime.ML Sat Apr 02 21:54:51 2016 +0200 +++ b/src/Pure/Isar/runtime.ML Sat Apr 02 21:55:32 2016 +0200 @@ -159,7 +159,7 @@ local fun print_entry (name, loc) = - Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_location loc)); + Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_polyml_location loc)); fun exception_debugger output e = let