src/Pure/Isar/proof_display.ML
changeset 17756 d4a35f82fbb4
parent 17369 dec2ddbb3edf
child 18799 f137c5e971f5
     1.1 --- a/src/Pure/Isar/proof_display.ML	Tue Oct 04 16:47:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Oct 04 19:01:37 2005 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  fun name_results "" res = res
     1.5    | name_results name res =
     1.6        let
     1.7 -        val n = length (List.concat (map #2 res));
     1.8 +        val n = length (List.concat (map snd res));
     1.9          fun name_res (a, ths) i =
    1.10            let
    1.11              val m = length ths;
    1.12 @@ -57,7 +57,7 @@
    1.13                ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
    1.14              else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
    1.15            end;
    1.16 -      in #1 (fold_map name_res res 1) end;
    1.17 +      in fst (fold_map name_res res 1) end;
    1.18  
    1.19  in
    1.20