[isabelle-dev] Towards release

[Alexander Krauss]

>> partial_function(option) foo :: "nat list \<Rightarrow> unit option"
>> where "foo x = foo x"
>>
>> works, but
>>
>> partial_function(option) foo :: "'a list \<Rightarrow> unit option"
>> where "foo x = foo x"
>>
>> yields the following error message.
>>
>> *** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type


> Alex seems to have fixed this issue with changeset 8b74cfea913a

Yes, many thanks for reporting this one. It came in when I added the 
generation of induction rules (which is still somewhat unfinished) in 
df41a5762c3d. This also shows that partial_function isn't terribly 
well-tested at the moment.

Alex