doc-src/TutorialI/Datatype/unfoldnested.thy

 (*<*)
 theory unfoldnested = Main:;
 (*>*)
-datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
-and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
+datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
+and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
 (*<*)
 end
 (*>*)