1.1 --- a/src/Pure/drule.ML	Tue Mar 21 17:43:54 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Mar 22 12:33:34 2000 +0100
     1.3 @@ -76,6 +76,7 @@
     1.4    val triv_forall_equality: thm
     1.5    val swap_prems_rl     : thm
     1.6    val equal_intr_rule   : thm
     1.7 +  val inst              : string -> string -> thm -> thm
     1.8    val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
     1.9    val incr_indexes      : int -> thm -> thm
    1.10    val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    1.11 @@ -629,6 +630,10 @@
    1.12  
    1.13  (** variations on instantiate **)
    1.14  
    1.15 +(*shorthand for instantiating just one variable in the current theory*)
    1.16 +fun inst x t = read_instantiate_sg (sign_of (the_context())) [(x,t)];
    1.17 +
    1.18 +
    1.19  (* collect vars *)
    1.20  
    1.21  val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);