src/Pure/Isar/proof_display.ML
changeset 26336 a0e2b706ce73
parent 24920 2a45e400fdad
child 26361 7946f459c6c8
     1.1 --- a/src/Pure/Isar/proof_display.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -111,8 +111,9 @@
     1.4              if a <> "" then ((a, ths), j)
     1.5              else if m = n then ((name, ths), j)
     1.6              else if m = 1 then
     1.7 -              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
     1.8 -            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
     1.9 +              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
    1.10 +            else
    1.11 +              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
    1.12            end;
    1.13        in fst (fold_map name_res res 1) end;
    1.14