parallel parsing of big specifications;
authorwenzelm
Wed, 06 Apr 2011 23:17:45 +0200
changeset 42265 ffdaa07cf6cf
parent 42264 b6c1b0c4c511
child 42266 f87e0be80a3f
parallel parsing of big specifications;
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);