--- 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;