--- a/src/Pure/drule.ML Fri Jan 19 22:08:16 2007 +0100
+++ b/src/Pure/drule.ML Fri Jan 19 22:08:18 2007 +0100
@@ -81,7 +81,6 @@
val equal_intr_rule: thm
val equal_elim_rule1: thm
val equal_elim_rule2: thm
- val inst: string -> string -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
end;
@@ -988,10 +987,6 @@
(** variations on instantiate **)
-(*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
-
-
(* instantiate by left-to-right occurrence of variables *)
fun instantiate' cTs cts thm =
--- a/src/Pure/old_goals.ML Fri Jan 19 22:08:16 2007 +0100
+++ b/src/Pure/old_goals.ML Fri Jan 19 22:08:18 2007 +0100
@@ -43,6 +43,7 @@
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 =
@@ -366,7 +367,7 @@
fun goal thy = goalw thy [];
(*now the versions that wrap the goal up in `Goal' to make it atomic*)
-fun Goalw thms s = agoalw true (Context.the_context ()) thms s;
+fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s;
val Goal = Goalw [];
(*simple version with minimal amount of checking and postprocessing*)
@@ -514,6 +515,9 @@
fun no_qed () = ();
+(*shorthand for instantiating just one variable in the current theory*)
+fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
+
end;
structure Goals: GOALS = OldGoals;