diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Simult.thy
--- a/ex/Simult.thy	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Simult.thy	Thu Aug 18 12:48:03 1994 +0200
@@ -3,8 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Primitives for simultaneous recursive type definitions
-  includes worked example of trees & forests
+A simultaneous recursive type definition: trees & forests
 
 This is essentially the same data structure that on ex/term.ML, which is
 simpler because it uses List as a new type former.  The approach in this
@@ -19,7 +18,6 @@
 arities  tree,forest :: (term)term
 
 consts
-  Part        :: "['a set, 'a=>'a] => 'a set"
   TF          :: "'a node set set => 'a node set set"
   FNIL        :: "'a node set"
   TCONS,FCONS :: "['a node set, 'a node set] => 'a node set"
@@ -38,9 +36,6 @@
 \                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
 
 rules
-    (*operator for selecting out the various types*)
-  Part_def	"Part(A,h) == {x. x:A & (? z. x = h(z))}"
-
   TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
 \                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
     (*faking a type definition for tree...*)
@@ -65,9 +60,8 @@
      (*recursion*)
   TF_rec_def	
    "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, 			\
-\               %Z g. Case(Z, %U. Split(U, %x y. b(x,y,g(y))),		\
-\			      %V. List_case(V, c, 			\
-\                                           %x y. d(x,y,g(x),g(y)))))"
+\               Case(Split(%x y g. b(x,y,g(y))),		\
+\	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
 
   tree_rec_def
    "tree_rec(t,b,c,d) == \