--- a/src/HOL/Tools/Function/partial_function.ML Mon Sep 19 23:34:22 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Sep 20 01:32:04 2011 +0200
@@ -258,7 +258,7 @@
val mk_raw_induct =
mk_curried_induct args args_ctxt (cert curry) (cert uncurry)
#> singleton (Variable.export args_ctxt lthy)
- #> (fn thm => Drule.instantiate' [] [SOME (cert F)] thm OF [mono_thm, f_def])
+ #> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [mono_thm, f_def])
#> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
val raw_induct = Option.map mk_raw_induct fixp_induct