# HG changeset patch
# User wenzelm
# Date 1723992392 -7200
# Node ID ea8d52d373136ad2784726fe1c4707298f863432
# Parent  f9b31d348fdead0424c62d3b6c10d7dda776e889
tuned: eliminate clone (with change of internal exceptions);

diff -r f9b31d348fde -r ea8d52d37313 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Aug 18 15:49:24 2024 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sun Aug 18 16:46:32 2024 +0200
@@ -74,10 +74,6 @@
   | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
   | zip3 _ _ _ = raise Fail "Choice_Specification.process_spec internal error"
 
-fun myfoldr f [x] = x
-  | myfoldr f (x::xs) = f (x,myfoldr f xs)
-  | myfoldr f [] = raise Fail "Choice_Specification.process_spec internal error"
-
 fun process_spec cos alt_props thy =
   let
     val ctxt = Proof_Context.init_global thy
@@ -97,7 +93,7 @@
 
     val props'' = map proc_single props'
     val frees = map snd props''
-    val prop = myfoldr HOLogic.mk_conj (map fst props'')
+    val prop = foldr1 HOLogic.mk_conj (map fst props'')
 
     val (vmap, prop_thawed) = Type.varify_global TFrees.empty prop
     val thawed_prop_consts = collect_consts (prop_thawed, [])