match types when applying mono_thm -- previous export generalizes type variables;
authorkrauss
Tue Sep 20 01:32:04 2011 +0200 (2011-09-20)
changeset 450088b74cfea913a
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
src/HOL/ex/Fundefs.thy
     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