# HG changeset patch
# User nipkow
# Date 860158120 -7200
# Node ID d1d5a0acbf7249ff33a488ce5b26cc3cb9b4802d
# Parent  bacef535265c0de3f20d77f8393d94123ef61515
Inv -> inv

diff -r bacef535265c -r d1d5a0acbf72 src/HOL/Subst/UTerm.ML
--- a/src/HOL/Subst/UTerm.ML	Fri Apr 04 14:47:26 1997 +0200
+++ b/src/HOL/Subst/UTerm.ML	Fri Apr 04 14:48:40 1997 +0200
@@ -247,7 +247,7 @@
 
 Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, 
           Abs_uterm_inverse, Rep_uterm_inverse, 
-          Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp];
+          Rep_uterm, rangeI, inj_Leaf, inv_f_f, Rep_uterm_in_sexp];
 
 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)";
 by (Simp_tac 1);
diff -r bacef535265c -r d1d5a0acbf72 src/HOL/Subst/UTerm.thy
--- 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