# HG changeset patch
# User wenzelm
# Date 1450090052 -3600
# Node ID c5c7bc41185caeba7d28de44758e269c6579a8c8
# Parent  007d3b34080f9fe82832c7c219f92f376954ed2b
tuned;

diff -r 007d3b34080f -r c5c7bc41185c src/HOL/Tools/Predicate_Compile/core_data.ML
--- 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)
diff -r 007d3b34080f -r c5c7bc41185c src/Pure/General/basics.ML
--- 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 *)