--- a/src/HOL/Tools/choice_specification.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Jul 27 17:44:55 2015 +0200
@@ -138,7 +138,7 @@
let
val cv = Thm.global_cterm_of thy v
val cT = Thm.ctyp_of_cterm cv
- val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
+ val spec' = Thm.instantiate' [SOME cT] [NONE, SOME cv] spec
in thm RS spec' end
fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
fun process_single ((name, atts), rew_imp, frees) args =