--- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 17:58:26 2009 +0100
@@ -143,7 +143,7 @@
val (_, c') = Type.varify [] c
val (cname,ctyp) = dest_Const c'
in
- case List.filter (fn t => let val (name,typ) = dest_Const t
+ case filter (fn t => let val (name,typ) = dest_Const t
in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
end) thawed_prop_consts of
[] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")