--- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:49:55 2009 +0100
+++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:56:33 2009 +0100
@@ -120,7 +120,8 @@
val frees = OldTerm.term_frees prop
val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
orelse error "Specificaton: Only free variables of sort 'type' allowed"
- val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
+ val prop_closed = fold_rev (fn (vname, T) => fn prop =>
+ HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop
in
(prop_closed,frees)
end
@@ -151,7 +152,7 @@
| _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
end
val proc_consts = map proc_const consts
- fun mk_exist (c,prop) =
+ fun mk_exist c prop =
let
val T = type_of c
val cname = Long_Name.base_name (fst (dest_Const c))
@@ -161,7 +162,7 @@
in
HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
end
- val ex_prop = List.foldr mk_exist prop proc_consts
+ val ex_prop = fold_rev mk_exist proc_consts prop
val cnames = map (fst o dest_Const) proc_consts
fun post_process (arg as (thy,thm)) =
let