[isabelle-dev] *** exception Empty raised (line 331 of "library.ML")

[Tobias Nipkow]

instantiation list :: (order) order
begin

fun le_list :: "('a::order)list => 'a list => bool" where
"le_list [] [] = True" |
"le_list (x#xs) (y#ys) = (x <= y & xs <= ys)" |
"le_list _ _ = False"

*** exception Empty raised (line 331 of "library.ML")

Of course it should be less_eq instead of le, but still...

Tobias