equal
deleted
inserted
replaced
240 case Symbol.explode str of |
240 case Symbol.explode str of |
241 "b"::"d"::"v"::_ => true |
241 "b"::"d"::"v"::_ => true |
242 | _ => false; |
242 | _ => false; |
243 fun is_bdv_ (Free (s,_)) = is_bdv s |
243 fun is_bdv_ (Free (s,_)) = is_bdv s |
244 | is_bdv_ _ = false; |
244 | is_bdv_ _ = false; |
|
245 |
|
246 (* is a term a substitution for a bdv as found in programs *) |
|
247 fun is_bdv_subst (Const ("List.list.Cons", _) $ |
|
248 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str |
|
249 | is_bdv_subst _ = false; |
245 |
250 |
246 fun free2str (Free (s,_)) = s |
251 fun free2str (Free (s,_)) = s |
247 | free2str t = error ("free2str not for "^ term2str t); |
252 | free2str t = error ("free2str not for "^ term2str t); |
248 fun free2int (t as Free (s, _)) = ((str2int s) |
253 fun free2int (t as Free (s, _)) = ((str2int s) |
249 handle _ => error ("free2int: "^term_detail2str t)) |
254 handle _ => error ("free2int: "^term_detail2str t)) |