# HG changeset patch
# User wenzelm
# Date 1169240898 -3600
# Node ID 9188aed2c3ca0b541af6d4d0883046e7790baf0f
# Parent  d76ea9928959a3093d039fb278c311ab1f306919
moved inst from drule.ML to old_goals.ML;

diff -r d76ea9928959 -r 9188aed2c3ca src/Pure/drule.ML
--- 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 =
diff -r d76ea9928959 -r 9188aed2c3ca src/Pure/old_goals.ML
--- 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;