diff -r 872f866e630f -r d9527f97246e ex/Term.thy
--- a/ex/Term.thy	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Term.thy	Thu Aug 25 10:47:33 1994 +0200
@@ -1,12 +1,12 @@
-(*  Title: 	HOL/ex/term
+(*  Title: 	HOL/ex/Term
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Terms over a given alphabet -- function applications; illustrates List functor
+Terms over a given alphabet -- function applications; illustrates list functor
   (essentially the same type as in Trees & Forests)
 
-There is no constructor APP because it is simply cons (.) 
+There is no constructor APP because it is simply cons ($) 
 *)
 
 Term = List +
@@ -16,33 +16,40 @@
 arities term :: (term)term
 
 consts
-  Term		:: "'a node set set => 'a node set set"
-  Rep_Term	:: "'a term => 'a node set"
-  Abs_Term	:: "'a node set => 'a term"
-  Rep_TList	:: "'a term list => 'a node set"
-  Abs_TList	:: "'a node set => 'a term list"
+  term		:: "'a item set => 'a item set"
+  Rep_term	:: "'a term => 'a item"
+  Abs_term	:: "'a item => 'a term"
+  Rep_Tlist	:: "'a term list => 'a item"
+  Abs_Tlist	:: "'a item => 'a term list"
   App		:: "['a, ('a term)list] => 'a term"
-  Term_rec	::
-    "['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
+  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
   term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
 
-rules
-  Term_def		"Term(A) == lfp(%Z.  A <*> List(Z))"
-    (*faking a type definition for term...*)
-  Rep_Term 		"Rep_Term(n): Term(range(Leaf))"
-  Rep_Term_inverse 	"Abs_Term(Rep_Term(t)) = t"
-  Abs_Term_inverse 	"M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
-    (*defining abstraction/representation functions for term list...*)
-  Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
-  Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
-    (*defining the abstract constants*)
-  App_def 	"App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
-     (*list recursion*)
+inductive "term(A)"
+  intrs
+    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
+  monos   "[list_mono]"
+
+defs
+  (*defining abstraction/representation functions for term list...*)
+  Rep_Tlist_def	"Rep_Tlist == Rep_map(Rep_term)"
+  Abs_Tlist_def	"Abs_Tlist == Abs_map(Abs_term)"
+
+  (*defining the abstract constants*)
+  App_def 	"App(a,ts) == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+
+  (*list recursion*)
   Term_rec_def	
-   "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
+   "Term_rec(M,d) == wfrec(trancl(pred_sexp),  M, \
 \            Split(%x y g. d(x,y, Abs_map(g,y))))"
 
   term_rec_def
    "term_rec(t,d) == \
-\   Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))"
+\   Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
+
+rules
+    (*faking a type definition for term...*)
+  Rep_term 		"Rep_term(n): term(range(Leaf))"
+  Rep_term_inverse 	"Abs_term(Rep_term(t)) = t"
+  Abs_term_inverse 	"M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
 end