ex/Term.thy
changeset 114 b7f57e0ab47c
parent 72 30e80f028c57
child 127 d9527f97246e
--- a/ex/Term.thy	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Term.thy	Thu Aug 18 12:48:03 1994 +0200
@@ -40,7 +40,7 @@
      (*list recursion*)
   Term_rec_def	
    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
-\            %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
+\            Split(%x y g. d(x,y, Abs_map(g,y))))"
 
   term_rec_def
    "term_rec(t,d) == \