equal
deleted
inserted
replaced
332 |
332 |
333 |
333 |
334 (* no_tvars *) |
334 (* no_tvars *) |
335 |
335 |
336 fun no_tvars T = |
336 fun no_tvars T = |
337 (case Term.add_tvarsT T [] of [] => T |
337 (case Term.add_tvarsT T [] of |
338 | vs => raise TYPE ("Illegal schematic type variable(s): " ^ |
338 [] => T |
339 commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); |
339 | vs => |
|
340 raise TYPE ("Illegal schematic type variable(s): " ^ |
|
341 commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); |
340 |
342 |
341 |
343 |
342 (* varify_global *) |
344 (* varify_global *) |
343 |
345 |
344 fun varify_global_names fixed t = |
346 fun varify_global_names fixed t = |