# 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, [])