doc-src/TutorialI/Datatype/unfoldnested.thy
changeset 10971 6852682eaf16
parent 8751 9ed0548177fb
child 16417 9bc16273c2d4
--- a/doc-src/TutorialI/Datatype/unfoldnested.thy	Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/unfoldnested.thy	Wed Jan 24 12:29:10 2001 +0100
@@ -1,8 +1,8 @@
 (*<*)
 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
 (*>*)