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