src/Pure/old_goals.ML
changeset 22109 9188aed2c3ca
parent 20872 528054ca23e3
child 22360 26ead7ed4f4b
     1.1 --- a/src/Pure/old_goals.ML	Fri Jan 19 22:08:16 2007 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Fri Jan 19 22:08:18 2007 +0100
     1.3 @@ -43,6 +43,7 @@
     1.4    val qed_goalw_spec_mp: string -> theory -> thm list -> string
     1.5      -> (thm list -> tactic list) -> unit
     1.6    val no_qed: unit -> unit
     1.7 +  val inst: string -> string -> thm -> thm
     1.8  end;
     1.9  
    1.10  signature OLD_GOALS =
    1.11 @@ -366,7 +367,7 @@
    1.12  fun goal thy = goalw thy [];
    1.13  
    1.14  (*now the versions that wrap the goal up in `Goal' to make it atomic*)
    1.15 -fun Goalw thms s = agoalw true (Context.the_context ()) thms s;
    1.16 +fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s;
    1.17  val Goal = Goalw [];
    1.18  
    1.19  (*simple version with minimal amount of checking and postprocessing*)
    1.20 @@ -514,6 +515,9 @@
    1.21  
    1.22  fun no_qed () = ();
    1.23  
    1.24 +(*shorthand for instantiating just one variable in the current theory*)
    1.25 +fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
    1.26 +
    1.27  end;
    1.28  
    1.29  structure Goals: GOALS = OldGoals;