# HG changeset patch
# User wenzelm
# Date 1538303622 -7200
# Node ID 051127c38be80afbe496da5424a02345b14ad662
# Parent  06017b2c4552749e2ce8642879ccfb57e7e21927
tuned -- eliminated clone;

diff -r 06017b2c4552 -r 051127c38be8 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Sun Sep 30 12:26:14 2018 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sun Sep 30 12:33:42 2018 +0200
@@ -63,14 +63,9 @@
            {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
            Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
 
-fun option_eq _ (NONE,NONE) = true
-  | option_eq _ (NONE,_) = false
-  | option_eq _ (_,NONE) = false
-  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
-
 fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
                 {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
-                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
+                Thm.eq_thm (quot_thm1, quot_thm2) andalso eq_option pcr_eq (pcr_info1, pcr_info2)
 
 fun join_restore_data key (rd1:restore_data, rd2) =
   if pointer_eq (rd1, rd2) then raise Symtab.SAME else