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