mk_primed_var : string * hol_type -> term

- STRUCTURE
- SYNOPSIS
- Primes a variable name sufficiently to make it distinct from all constants.
- DESCRIPTION
- When applied to a record made from a string v and a type ty, the function mk_primed_var constructs a variable whose name consists of v followed by however many primes are necessary to make it distinct from any constants in the current theory.
- FAILURE
- Never fails.
- EXAMPLE
- new_theory "wombat"; > val it = () : unit - mk_primed_var("x", bool); > val it = `x` : term - new_constant("x", alpha); > val it = () : unit - mk_primed_var("x", bool); > val it = `x'` : term

- SEEALSO

HOL Kananaskis-14