src/Pure/goals.ML

--- a/src/Pure/goals.ML	Fri Feb 16 12:08:49 1996 +0100
+++ b/src/Pure/goals.ML	Fri Feb 16 12:19:47 1996 +0100
@@ -12,8 +12,6 @@
 
 signature GOALS =
   sig
-  structure Tactical: TACTICAL
-  local open Tactical Tactical.Thm in
   type proof
   val ba		: int -> unit
   val back		: unit -> unit
@@ -66,17 +64,10 @@
   val save_proof	: unit -> proof
   val topthm		: unit -> thm
   val undo		: unit -> unit
-  end
   end;
 
-functor GoalsFun (structure Logic: LOGIC and Drule: DRULE and Tactic: TACTIC
-                        and Pattern:PATTERN
-	  sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig
-              and Drule.Thm = Tactic.Tactical.Thm) : GOALS =
+structure Goals : GOALS =
 struct
-structure Tactical = Tactic.Tactical
-local open Tactic Tactic.Tactical Tactic.Tactical.Thm Drule
-in
 
 (*Each level of goal stack includes a proof state and alternative states,
   the output of the tactic applied to the preceeding level.  *)
@@ -154,7 +145,7 @@
                  cat_lines (map (Sign.string_of_term sign) hyps))
 	    else if not (null xshyps) then result_error state
                 ("Extra sort hypotheses: " ^
-                 commas (map Sign.Type.str_of_sort xshyps))
+                 commas (map Type.str_of_sort xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th 
@@ -199,7 +190,7 @@
   let val (prems, st0, mkresult) = prepare_proof rths chorn
       val tac = EVERY (tacsf prems)
       fun statef() = 
-	  (case Sequence.pull (tapply(tac,st0)) of 
+	  (case Sequence.pull (tac st0) of 
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
   in  mkresult (true, cond_timeit (!proof_timing) statef)  end
@@ -270,7 +261,7 @@
 local exception GETHYPS of thm list
 in
 fun gethyps i = 
-    (tapply(METAHYPS (fn hyps => raise (GETHYPS hyps)) i, topthm());  [])
+    (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm());  [])
     handle GETHYPS hyps => hyps
 end;
 
@@ -316,7 +307,7 @@
 
 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
 fun by_com tac ((th,ths), pairs) : gstack =
-  (case  Sequence.pull(tapply(tac, th))  of
+  (case  Sequence.pull(tac th)  of
      None      => error"by: tactic failed"
    | Some(th2,ths2) => 
        (if eq_thm(th,th2) 
@@ -444,4 +435,5 @@
 fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
 
 end;
-end;
+
+open Goals;