moved inst from drule.ML to old_goals.ML;
authorwenzelm
Fri Jan 19 22:08:18 2007 +0100 (2007-01-19)
changeset 221099188aed2c3ca
parent 22108 d76ea9928959
child 22110 f9eb6328bdbd
moved inst from drule.ML to old_goals.ML;
src/Pure/drule.ML
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/drule.ML	Fri Jan 19 22:08:16 2007 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Jan 19 22:08:18 2007 +0100
     1.3 @@ -81,7 +81,6 @@
     1.4    val equal_intr_rule: thm
     1.5    val equal_elim_rule1: thm
     1.6    val equal_elim_rule2: thm
     1.7 -  val inst: string -> string -> thm -> thm
     1.8    val instantiate': ctyp option list -> cterm option list -> thm -> thm
     1.9  end;
    1.10  
    1.11 @@ -988,10 +987,6 @@
    1.12  
    1.13  (** variations on instantiate **)
    1.14  
    1.15 -(*shorthand for instantiating just one variable in the current theory*)
    1.16 -fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
    1.17 -
    1.18 -
    1.19  (* instantiate by left-to-right occurrence of variables *)
    1.20  
    1.21  fun instantiate' cTs cts thm =
     2.1 --- a/src/Pure/old_goals.ML	Fri Jan 19 22:08:16 2007 +0100
     2.2 +++ b/src/Pure/old_goals.ML	Fri Jan 19 22:08:18 2007 +0100
     2.3 @@ -43,6 +43,7 @@
     2.4    val qed_goalw_spec_mp: string -> theory -> thm list -> string
     2.5      -> (thm list -> tactic list) -> unit
     2.6    val no_qed: unit -> unit
     2.7 +  val inst: string -> string -> thm -> thm
     2.8  end;
     2.9  
    2.10  signature OLD_GOALS =
    2.11 @@ -366,7 +367,7 @@
    2.12  fun goal thy = goalw thy [];
    2.13  
    2.14  (*now the versions that wrap the goal up in `Goal' to make it atomic*)
    2.15 -fun Goalw thms s = agoalw true (Context.the_context ()) thms s;
    2.16 +fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s;
    2.17  val Goal = Goalw [];
    2.18  
    2.19  (*simple version with minimal amount of checking and postprocessing*)
    2.20 @@ -514,6 +515,9 @@
    2.21  
    2.22  fun no_qed () = ();
    2.23  
    2.24 +(*shorthand for instantiating just one variable in the current theory*)
    2.25 +fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
    2.26 +
    2.27  end;
    2.28  
    2.29  structure Goals: GOALS = OldGoals;