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