--- a/src/Pure/Isar/proof_display.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Oct 04 19:01:37 2005 +0200
@@ -45,7 +45,7 @@
fun name_results "" res = res
| name_results name res =
let
- val n = length (List.concat (map #2 res));
+ val n = length (List.concat (map snd res));
fun name_res (a, ths) i =
let
val m = length ths;
@@ -57,7 +57,7 @@
((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
end;
- in #1 (fold_map name_res res 1) end;
+ in fst (fold_map name_res res 1) end;
in