[isabelle] Types for Function.get_info

Hi all,

While using "Function.get_info" in Isabelle/HOL(ML), I got an "Empty" 
exception coming from the "the_single" function.

I discovered that when defining a function in Isabelle/HOL, as soon as the 
type variables of the type annotation differs from the ones of the infered 
type (without type annotation), the function is added twice (with these two 
typing informations) to the FunctionData. Then the "the_single" call of 
"Function.get_info" fails (with an Empty exception while the list contains 2 
elements, which can be a little confusing :-)).

Here is a simple example:

fun foo :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b)" where
  "foo a b = (a, b)"

ML {*
  Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo"}
  |> map #1
*} (* 1 element in the list *)

fun foo' :: "'a \<Rightarrow> 'c \<Rightarrow> ('a * 'c)" where
  "foo' a b = (a, b)"

ML {*
  Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo'"}
  |> map #1
*} (* 2 elements with similar types in the list *)

ML {* Function.get_info @{context} @{term "foo"} *} (* OK *)
ML {* Function.get_info @{context} @{term "foo'"} *} (* exception Empty *)

Bug or feature ?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.