equal
deleted
inserted
replaced
109 |
109 |
110 (* ------------------------------------------------------------------------- *) |
110 (* ------------------------------------------------------------------------- *) |
111 (* The size of a term in symbols. *) |
111 (* The size of a term in symbols. *) |
112 (* ------------------------------------------------------------------------- *) |
112 (* ------------------------------------------------------------------------- *) |
113 |
113 |
|
114 val VAR_SYMBOLS = 1; |
|
115 |
|
116 val FN_SYMBOLS = 1; |
|
117 |
114 local |
118 local |
115 fun sz n [] = n |
119 fun sz n [] = n |
116 | sz n (Var _ :: tms) = sz (n + 1) tms |
120 | sz n (Var _ :: tms) = sz (n + VAR_SYMBOLS) tms |
117 | sz n (Fn (_,args) :: tms) = sz (n + 1) (args @ tms); |
121 | sz n (Fn (func,args) :: tms) = sz (n + FN_SYMBOLS) (args @ tms); |
118 in |
122 in |
119 fun symbols tm = sz 0 [tm]; |
123 fun symbols tm = sz 0 [tm]; |
120 end; |
124 end; |
121 |
125 |
122 (* ------------------------------------------------------------------------- *) |
126 (* ------------------------------------------------------------------------- *) |