diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Subst.thy	Thu May 15 12:40:01 1997 +0200
@@ -5,33 +5,35 @@
 Substitutions on uterms
 *)
 
-Subst = Setplus + AList + UTLemmas +
+Subst = AList + UTerm +
 
 consts
 
-  "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
-
-  "<|"   ::  "['a uterm,('a*('a uterm)) list] => 'a uterm"         (infixl 55)
-  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => 
-                                    ('a*('a uterm)) list"         (infixl 56)
+  "=$="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
+  "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
+  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] 
+                 => ('a*('a uterm)) list"                          (infixl 56)
   sdom   ::  "('a*('a uterm)) list => 'a set"
   srange ::  "('a*('a uterm)) list => 'a set"
 
-rules 
 
-  subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
+primrec "op <|"   uterm
+  subst_Var      "(Var v <| s) = assoc v (Var v) s"
+  subst_Const  "(Const c <| s) = Const c"
+  subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
 
-  subst_def    
-  "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
-                         (%x.Const(x))                  
-                         (%u v q r.Comb q r)"
+
+defs 
 
-  comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
+  subst_eq_def  "r =$= s == ALL t.t <| r = t <| s"
+
+  comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
 
   sdom_def
   "sdom(al) == alist_rec al {}  
-                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
+                (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
+
   srange_def   
-  "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
+   "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
 
 end