1
(*<*)
2
theory unfoldnested imports Main begin
3
(*>*)
4
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
5
and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
6
7
end
8