# HG changeset patch
# User kuncar
# Date 1353935748 -3600
# Node ID f478f4ca7f193aeae955d05e88ff9a9aa6a80ab0
# Parent  aacd6da0982584d0e1eb6f6b54179abc181aea39
add option_fold

diff -r aacd6da09825 -r f478f4ca7f19 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Nov 26 14:11:31 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Nov 26 14:15:48 2012 +0100
@@ -8,6 +8,7 @@
 sig
   val MRSL: thm list * thm -> thm
   val Trueprop_conv: conv -> conv
+  val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
   val dest_Quotient: term -> term * term * term * term
 
   val quot_thm_rel: thm -> term
@@ -29,6 +30,9 @@
     Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
   | _ => raise CTERM ("Trueprop_conv", [ct]))
 
+fun option_fold a _ NONE = a
+  | option_fold _ f (SOME x) = f x
+
 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
       = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])