# HG changeset patch
# User wenzelm
# Date 1313929004 -7200
# Node ID 02f286491568f8f09c45a924678b4617f8dfa821
# Parent  176e0fb6906b4124c91bd09f430f4d3bf9282032
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;

diff -r 176e0fb6906b -r 02f286491568 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Aug 21 13:42:55 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Aug 21 14:16:44 2011 +0200
@@ -175,9 +175,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val elements =
       Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
-      |> Par_List.map_name "Outer_Syntax.prepare_element"
-        (Outer_Syntax.prepare_element outer_syntax init)
-      |> flat;
+      |> maps (Outer_Syntax.prepare_element outer_syntax init);
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);