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

     2.1 --- a/src/HOL/ex/Fundefs.thy	Mon Sep 19 23:34:22 2011 +0200
     2.2 +++ b/src/HOL/ex/Fundefs.thy	Tue Sep 20 01:32:04 2011 +0200
     2.3 @@ -387,4 +387,9 @@
     2.4  | "f4 _ _ = False"
     2.5  
     2.6  
     2.7 +(* polymorphic partial_function *)
     2.8 +partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
     2.9 +where
    2.10 +  "f5 x = f5 x"
    2.11 +
    2.12  end