--- a/src/Pure/Isar/proof_display.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML Wed Mar 19 22:27:57 2008 +0100
@@ -111,8 +111,9 @@
if a <> "" then ((a, ths), j)
else if m = n then ((name, ths), j)
else if m = 1 then
- ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
- else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
+ ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
+ else
+ ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
end;
in fst (fold_map name_res res 1) end;