# HG changeset patch
# User wenzelm
# Date 1213631687 -7200
# Node ID 224c830e7abe3f4c7dc9679d395f27114de1e8e2
# Parent  7cd256da0a36b4970dc105b69a0bd05e161b4500
removed obsolete inst;

diff -r 7cd256da0a36 -r 224c830e7abe src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Mon Jun 16 17:54:46 2008 +0200
+++ b/src/Pure/old_goals.ML	Mon Jun 16 17:54:47 2008 +0200
@@ -81,7 +81,6 @@
   val fds: thm list -> unit
   val fd: thm -> unit
   val fa: unit -> unit
-  val inst: string -> string -> thm -> thm
 end;
 
 structure OldGoals: OLD_GOALS =
@@ -517,9 +516,6 @@
 
 fun no_qed () = ();
 
-(*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = Drule.read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
-
 end;
 
 structure Goals: GOALS = OldGoals;