--- 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;
--- 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 =
--- 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;
--- 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)