53 (* raw_term_sorts *) |
53 (* raw_term_sorts *) |
54 |
54 |
55 fun raw_term_sorts tm = |
55 fun raw_term_sorts tm = |
56 let |
56 let |
57 fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = |
57 fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = |
58 ((x, ~1), sort_of_term cs) ins env |
58 insert (op =) ((x, ~1), sort_of_term cs) env |
59 | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env = |
59 | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env = |
60 ((x, ~1), sort_of_term cs) ins env |
60 insert (op =) ((x, ~1), sort_of_term cs) env |
61 | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = |
61 | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = |
62 (xi, sort_of_term cs) ins env |
62 insert (op =) (xi, sort_of_term cs) env |
63 | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env = |
63 | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env = |
64 (xi, sort_of_term cs) ins env |
64 insert (op =) (xi, sort_of_term cs) env |
65 | add_env (Abs (_, _, t)) env = add_env t env |
65 | add_env (Abs (_, _, t)) env = add_env t env |
66 | add_env (t1 $ t2) env = add_env t1 (add_env t2 env) |
66 | add_env (t1 $ t2) env = add_env t1 (add_env t2 env) |
67 | add_env _ env = env; |
67 | add_env _ env = env; |
68 in add_env tm [] end; |
68 in add_env tm [] end; |
69 |
69 |