equal
deleted
inserted
replaced
134 fun make_schematic_type_var (x,i) = |
134 fun make_schematic_type_var (x,i) = |
135 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
135 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
136 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
136 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
137 |
137 |
138 fun make_fixed_const c = |
138 fun make_fixed_const c = |
139 case Symtab.lookup (const_trans_table,c) of |
139 case Symtab.curried_lookup const_trans_table c of |
140 SOME c' => c' |
140 SOME c' => c' |
141 | NONE => const_prefix ^ (ascii_of c); |
141 | NONE => const_prefix ^ ascii_of c; |
142 |
142 |
143 fun make_fixed_type_const c = |
143 fun make_fixed_type_const c = |
144 case Symtab.lookup (type_const_trans_table,c) of |
144 case Symtab.curried_lookup type_const_trans_table c of |
145 SOME c' => c' |
145 SOME c' => c' |
146 | NONE => tconst_prefix ^ (ascii_of c); |
146 | NONE => tconst_prefix ^ ascii_of c; |
147 |
147 |
148 fun make_type_class clas = class_prefix ^ (ascii_of clas); |
148 fun make_type_class clas = class_prefix ^ ascii_of clas; |
149 |
149 |
150 |
150 |
151 |
151 |
152 (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
152 (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
153 |
153 |