258 fun is_bdv_subst (Const ("List.list.Cons", _) $ |
258 fun is_bdv_subst (Const ("List.list.Cons", _) $ |
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 |
264 fun str_of_free_opt (Free (s,_)) = SOME s |
265 | str_of_free_opt _ = NONE |
265 | str_of_free_opt _ = NONE |
266 fun free2int (t as Free (s, _)) = ((str2int s) |
266 fun free2int (t as Free (s, _)) = ((str2int s) |
267 handle _ => error ("free2int: "^term_detail2str t)) |
267 handle _ => error ("free2int: " ^ term_detail2str t)) |
268 | free2int t = error ("free2int: "^term_detail2str t); |
268 | free2int t = error ("free2int: " ^ term_detail2str t); |
269 |
269 |
270 (*compare Logic.unvarify_global, which rejects Free*) |
270 (*compare Logic.unvarify_global, which rejects Free*) |
271 fun var2free (t as Const(s,T)) = t |
271 fun var2free (t as Const(s,T)) = t |
272 | var2free (t as Free(s,T)) = t |
272 | var2free (t as Free(s,T)) = t |
273 | var2free (Var((s,i),T)) = Free(s,T) |
273 | var2free (Var((s,i),T)) = Free(s,T) |