src/Pure/old_goals.ML

   val qed_spec_mp: string -> unit
   val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
   val qed_goalw_spec_mp: string -> theory -> thm list -> string
     -> (thm list -> tactic list) -> unit
   val no_qed: unit -> unit
-  val inst: string -> string -> thm -> thm
 end;
 
 signature OLD_GOALS =
 sig
   include GOALS

   val fes: thm list -> unit
   val fe: thm -> unit
   val fds: thm list -> unit
   val fd: thm -> unit
   val fa: unit -> unit
+  val inst: string -> string -> thm -> thm
 end;
 
 structure OldGoals: OLD_GOALS =
 struct
 

   bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
 
 fun no_qed () = ();
 
 (*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
+fun inst x t = Drule.read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
 
 end;
 
 structure Goals: GOALS = OldGoals;
 open Goals;