equal
deleted
inserted
replaced
259 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str |
259 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str |
260 | is_bdv_subst _ = false; |
260 | is_bdv_subst _ = false; |
261 |
261 |
262 fun free2str (Free (s,_)) = s |
262 fun free2str (Free (s,_)) = s |
263 | free2str t = error ("free2str not for "^ term2str t); |
263 | free2str t = error ("free2str not for "^ term2str t); |
|
264 fun str_of_free_opt (Free (s,_)) = SOME s |
|
265 | str_of_free_opt _ = NONE |
264 fun free2int (t as Free (s, _)) = ((str2int s) |
266 fun free2int (t as Free (s, _)) = ((str2int s) |
265 handle _ => error ("free2int: "^term_detail2str t)) |
267 handle _ => error ("free2int: "^term_detail2str t)) |
266 | free2int t = error ("free2int: "^term_detail2str t); |
268 | free2int t = error ("free2int: "^term_detail2str t); |
267 |
269 |
268 (*compare Logic.unvarify_global, which rejects Free*) |
270 (*compare Logic.unvarify_global, which rejects Free*) |