src/Pure/Isar/proof_display.ML
changeset 26361 7946f459c6c8
parent 26336 a0e2b706ce73
child 26415 1b624d6e9163
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Mar 20 12:09:22 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Mar 20 16:04:30 2008 +0100
     1.3 @@ -110,10 +110,8 @@
     1.4            in
     1.5              if a <> "" then ((a, ths), j)
     1.6              else if m = n then ((name, ths), j)
     1.7 -            else if m = 1 then
     1.8 -              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
     1.9 -            else
    1.10 -              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
    1.11 +            else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
    1.12 +              SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
    1.13            end;
    1.14        in fst (fold_map name_res res 1) end;
    1.15