[isabelle] rep_datatype and Datatype exception

Hello all,

I'm trying to use rep_datatype command, however I'm getting an exception 
"Datatype" and I'm not sure why.

In the following example, the only difference between Cons2 and Cons2' is the 
(un)currying of the parameters but it's OK for the first one while it isn't 
for the second.

theory RepDatatype imports Main

typedef 'a list2 = "UNIV:: 'a list set" ..

definition Nil2 :: "'a list2" where "Nil2 = Abs_list2 []"

fun Cons2 :: "'a \<Rightarrow> 'a list2 \<Rightarrow> 'a list2" where
  "Cons2 a as = Abs_list2 (a # Rep_list2 as)"

rep_datatype Nil2 Cons2 (* OK *)

fun Cons2' :: "('a * 'a list2) \<Rightarrow> 'a list2" where
  "Cons2' (a, as) = Abs_list2 (a # Rep_list2 as)"

rep_datatype Nil2 Cons2' (* exception Datatype raised
	(line 218 of "~~/src/HOL/Tools/Datatype/datatype_aux.ML") *)

What does this exception mean ?


Mathieu Giorgino

Attachment: signature.asc
Description: This is a digitally signed message part.

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