equal
deleted
inserted
replaced
1641 accum |
1641 accum |
1642 fun add_iterm_syms top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = |
1642 fun add_iterm_syms top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = |
1643 let val (head, args) = strip_iterm_comb tm in |
1643 let val (head, args) = strip_iterm_comb tm in |
1644 (case head of |
1644 (case head of |
1645 IConst ((s, _), T, _) => |
1645 IConst ((s, _), T, _) => |
1646 if is_maybe_universal_name s then |
1646 if is_maybe_universal_name s orelse String.isPrefix let_bound_var_prefix s then |
1647 add_universal_var T accum |
1647 add_universal_var T accum |
1648 else if String.isPrefix exist_bound_var_prefix s then |
1648 else if String.isPrefix exist_bound_var_prefix s then |
1649 accum |
1649 accum |
1650 else |
1650 else |
1651 let val ary = length args in |
1651 let val ary = length args in |