Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
match types when applying mono_thm -- previous export generalizes type variables;
authorkrauss
Tue, 20 Sep 2011 01:32:04 +0200
changeset 45008 8b74cfea913a
parent 45007 cc86edb97c2c
child 45009 99e1965f9c21
child 45014 0e847655b2d8
match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test
src/HOL/Tools/Function/partial_function.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Fundefs.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle