src/HOL/Subst/Subst.thy

--- a/src/HOL/Subst/Subst.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/Subst.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
   srange ::  "('a*('a uterm)) list => 'a set"
 
 
-primrec "op <|"   uterm
+primrec
   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)"