src/HOL/ex/Term.thy
changeset 2911 8a680e310f04
parent 1476 608483c2122a
--- a/src/HOL/ex/Term.thy	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/Term.thy	Fri Apr 04 16:27:39 1997 +0200
@@ -45,7 +45,7 @@
 
   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...*)