--- a/src/Pure/drule.ML Fri Jan 19 22:08:16 2007 +0100
+++ b/src/Pure/drule.ML Fri Jan 19 22:08:18 2007 +0100
@@ -81,7 +81,6 @@
val equal_intr_rule: thm
val equal_elim_rule1: thm
val equal_elim_rule2: thm
- val inst: string -> string -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
end;
@@ -988,10 +987,6 @@
(** variations on instantiate **)
-(*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
-
-
(* instantiate by left-to-right occurrence of variables *)
fun instantiate' cTs cts thm =