changeset 2903 | d1d5a0acbf72 |
parent 1476 | 608483c2122a |
child 3192 | a75558a4ed37 |
--- a/src/HOL/Subst/UTerm.thy Fri Apr 04 14:47:26 1997 +0200 +++ b/src/HOL/Subst/UTerm.thy Fri Apr 04 14:48:40 1997 +0200 @@ -59,7 +59,7 @@ uterm_rec_def "uterm_rec t b c d == - UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) + UTerm_rec (Rep_uterm t) (%x.b(inv Leaf x)) (%x.c(inv Leaf x)) (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)" end