diff -r cc86edb97c2c -r 8b74cfea913a src/HOL/Tools/Function/partial_function.ML
--- 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