# HG changeset patch
# User wenzelm
# Date 1302124665 -7200
# Node ID ffdaa07cf6cf793caf24ad9c6c1ad007c163a840
# Parent  b6c1b0c4c5114d9c7a1800bd2d7b97deedd0a67e
parallel parsing of big specifications;

diff -r b6c1b0c4c511 -r ffdaa07cf6cf src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 06 23:04:00 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 06 23:17:45 2011 +0200
@@ -122,7 +122,9 @@
     val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
     val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
 
-    val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
+    val Asss =
+      (map o map) snd raw_specss
+      |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt));
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
       |> fold Name.declare xs;
     val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);