# HG changeset patch
# User wenzelm
# Date 1231249415 -3600
# Node ID 503ce3f8f092e54ea5058d6f1185d35421eb8a1f
# Parent  741373421318920d2f26acc4653aaae36cb10f39
renamed structure ParList to Par_List;

diff -r 741373421318 -r 503ce3f8f092 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Jan 06 14:33:49 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Jan 06 14:43:35 2009 +0100
@@ -456,7 +456,7 @@
           |> fold (mark_seen o #1) new_facts
           |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
           |>> map_filter I;
-        val cache_entries = ParList.map skolem_cnfs defs;
+        val cache_entries = Par_List.map skolem_cnfs defs;
       in SOME (fold update_cache cache_entries thy') end
   end;
 
diff -r 741373421318 -r 503ce3f8f092 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Jan 06 14:33:49 2009 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Tue Jan 06 14:43:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Concurrent/par_list.ML
-    ID:         $Id$
     Author:     Makarius
 
 Parallel list combinators.
@@ -24,7 +23,7 @@
   val forall: ('a -> bool) -> 'a list -> bool
 end;
 
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
 struct
 
 fun raw_map f xs =
diff -r 741373421318 -r 503ce3f8f092 src/Pure/Concurrent/par_list_dummy.ML
--- a/src/Pure/Concurrent/par_list_dummy.ML	Tue Jan 06 14:33:49 2009 +0100
+++ b/src/Pure/Concurrent/par_list_dummy.ML	Tue Jan 06 14:43:35 2009 +0100
@@ -1,11 +1,10 @@
 (*  Title:      Pure/Concurrent/par_list_dummy.ML
-    ID:         $Id$
     Author:     Makarius
 
 Dummy version of parallel list combinators -- plain sequential evaluation.
 *)
 
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
 struct
 
 val map = map;
diff -r 741373421318 -r 503ce3f8f092 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jan 06 14:33:49 2009 +0100
+++ b/src/Pure/context.ML	Tue Jan 06 14:43:35 2009 +0100
@@ -135,7 +135,7 @@
 
 fun merge_data pp (data1, data2) =
   Datatab.keys (Datatab.merge (K true) (data1, data2))
-  |> ParList.map (fn k =>
+  |> Par_List.map (fn k =>
     (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
       (SOME x, NONE) => (k, invoke_extend k x)
     | (NONE, SOME y) => (k, invoke_extend k y)