src/Pure/Isar/proof_display.ML

         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
 
 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;
             val j = i + m;
           in

             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)
           end;
-      in #1 (fold_map name_res res 1) end;
+      in fst (fold_map name_res res 1) end;
 
 in
 
 fun print_results true = Pretty.writeln oo pretty_results
   | print_results false = K (K ());