Thanks Alex, the fixed version works again for IsaFoR Am 20.09.2011 um 11:22 schrieb 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 > -- René Thiemann mailto:[email protected] Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-6434 University of Innsbruck _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
