--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Jan 08 17:14:48 2011 +0100
@@ -81,7 +81,7 @@
fun merge_global_limit (NONE, NONE) = NONE
| merge_global_limit (NONE, SOME n) = SOME n
| merge_global_limit (SOME n, NONE) = SOME n
- | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
+ | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m)) (* FIXME odd merge *)
structure Options = Theory_Data
(
@@ -96,7 +96,7 @@
{ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
limited_types = limited_types2, limited_predicates = limited_predicates2,
replacing = replacing2, manual_reorder = manual_reorder2}) =
- {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ {ensure_groundness = ensure_groundness1 orelse ensure_groundness2 (* FIXME odd merge *),
limit_globally = merge_global_limit (limit_globally1, limit_globally2),
limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
@@ -122,9 +122,7 @@
type T = system_configuration
val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
val extend = I;
- fun merge ({timeout = timeout1, prolog_system = prolog_system1},
- {timeout = timeout2, prolog_system = prolog_system2}) =
- {timeout = timeout1, prolog_system = prolog_system1}
+ fun merge (a, _) = a
)
(* general string functions *)