--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Dec 14 11:20:31 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Dec 14 11:47:32 2015 +0100
@@ -123,10 +123,6 @@
mk_pred_data
(f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))))
-fun eq_option eq (NONE, NONE) = true
- | eq_option eq (SOME x, SOME y) = eq (x, y)
- | eq_option eq _ = false
-
fun eq_pred_data (PredData d1, PredData d2) =
eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
eq_option Thm.eq_thm (#elim d1, #elim d2)
--- a/src/Pure/General/basics.ML Mon Dec 14 11:20:31 2015 +0100
+++ b/src/Pure/General/basics.ML Mon Dec 14 11:47:32 2015 +0100
@@ -32,6 +32,7 @@
val the_default: 'a -> 'a option -> 'a
val perhaps: ('a -> 'a option) -> 'a -> 'a
val merge_options: 'a option * 'a option -> 'a option
+ val eq_option: ('a * 'b -> bool) -> 'a option * 'b option -> bool
(*partiality*)
val try: ('a -> 'b) -> 'a -> 'b option
@@ -93,6 +94,10 @@
fun merge_options (x, y) = if is_some x then x else y;
+fun eq_option eq (SOME x, SOME y) = eq (x, y)
+ | eq_option _ (NONE, NONE) = true
+ | eq_option _ _ = false;
+
(* partiality *)