# HG changeset patch
# User wenzelm
# Date 1213200218 -7200
# Node ID 0ddb5576b3874b53f1ac5d66fd58aab22981b277
# Parent  e9f2d5947887ba857a4ea77a531d175579ccf118
qualified inst;

diff -r e9f2d5947887 -r 0ddb5576b387 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Wed Jun 11 18:03:14 2008 +0200
+++ b/src/Pure/old_goals.ML	Wed Jun 11 18:03:38 2008 +0200
@@ -40,7 +40,6 @@
   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 =
@@ -82,6 +81,7 @@
   val fds: thm list -> unit
   val fd: thm -> unit
   val fa: unit -> unit
+  val inst: string -> string -> thm -> thm
 end;
 
 structure OldGoals: OLD_GOALS =
@@ -518,7 +518,7 @@
 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;