ex/term.thy
changeset 48 21291189b51e
parent 0 7949f97df77a
--- a/ex/term.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/term.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -32,7 +32,7 @@
   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))"
+  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, \