# HG changeset patch
# User krauss
# Date 1316475124 -7200
# Node ID 8b74cfea913ac21121b98a996c99e107cb4a9b87
# Parent  cc86edb97c2c4cb0146ab9f64e316eee950e6c8d
match types when applying mono_thm -- previous export generalizes type variables;
added trivial regression test

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
diff -r cc86edb97c2c -r 8b74cfea913a src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Sep 19 23:34:22 2011 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Sep 20 01:32:04 2011 +0200
@@ -387,4 +387,9 @@
 | "f4 _ _ = False"
 
 
+(* polymorphic partial_function *)
+partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
+where
+  "f5 x = f5 x"
+
 end