src/Pure/tactic.ML
changeset 4270 957c887b89b5
parent 4213 cef5ef41e70d
child 4438 ecfeff48bf0c
     1.1 --- a/src/Pure/tactic.ML	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4    val net_resolve_tac	: thm list -> int -> tactic
     1.5    val orderlist		: (int * 'a) list -> 'a list
     1.6    val PRIMITIVE		: (thm -> thm) -> tactic  
     1.7 -  val PRIMSEQ		: (thm -> thm Sequence.seq) -> tactic  
     1.8 +  val PRIMSEQ		: (thm -> thm Seq.seq) -> tactic  
     1.9    val prune_params_tac	: tactic
    1.10    val rename_tac	: string -> int -> tactic
    1.11    val rename_last_tac	: string -> string list -> int -> tactic
    1.12 @@ -99,10 +99,10 @@
    1.13  
    1.14  (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    1.15  fun trace_goalno_tac tac i st =  
    1.16 -    case Sequence.pull(tac i st) of
    1.17 -	None    => Sequence.null
    1.18 +    case Seq.pull(tac i st) of
    1.19 +	None    => Seq.empty
    1.20        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    1.21 -    			 Sequence.seqof(fn()=> seqcell));
    1.22 +    			 Seq.make(fn()=> seqcell));
    1.23  
    1.24  
    1.25  (*Convert all Vars in a theorem to Frees.  Also return a function for 
    1.26 @@ -137,15 +137,15 @@
    1.27      in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
    1.28          |> implies_intr_list (List.take(hyps, i-1) @ hyps')
    1.29          |> thaw
    1.30 -        |> Sequence.single
    1.31 +        |> Seq.single
    1.32      end
    1.33 -    handle _ => Sequence.null;
    1.34 +    handle _ => Seq.empty;
    1.35  
    1.36  
    1.37  (*Makes a rule by applying a tactic to an existing rule*)
    1.38  fun rule_by_tactic tac rl =
    1.39    let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
    1.40 -  in case Sequence.pull (tac st)  of
    1.41 +  in case Seq.pull (tac st)  of
    1.42  	None        => raise THM("rule_by_tactic", 0, [rl])
    1.43        | Some(st',_) => Thm.varifyT (thaw st')
    1.44    end;
    1.45 @@ -153,10 +153,10 @@
    1.46  (*** Basic tactics ***)
    1.47  
    1.48  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    1.49 -fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
    1.50 +fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    1.51  
    1.52  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    1.53 -fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
    1.54 +fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
    1.55  
    1.56  (*** The following fail if the goal number is out of range:
    1.57       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
    1.58 @@ -221,7 +221,7 @@
    1.59  	val assumed = implies_elim_list frozth (map assume froz_prems)
    1.60  	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
    1.61  					assumed;
    1.62 -    in  Sequence.single (thawfn implied)  end
    1.63 +    in  Seq.single (thawfn implied)  end
    1.64  end; 
    1.65  
    1.66  
    1.67 @@ -315,7 +315,7 @@
    1.68  	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.69  			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    1.70        val arg = (false, rl, nprems_of rl)
    1.71 -      val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
    1.72 +      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
    1.73    in  th  end
    1.74    handle Bind => raise THM("make_elim_preserve", 1, [rl]);
    1.75  
    1.76 @@ -352,12 +352,12 @@
    1.77  
    1.78  (*Introduce the given proposition as a lemma and subgoal*)
    1.79  fun subgoal_tac sprop i st = 
    1.80 -  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    1.81 +  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    1.82        val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
    1.83    in  
    1.84        if null (term_tvars concl') then ()
    1.85        else warning"Type variables in new subgoal: add a type constraint?";
    1.86 -      Sequence.single st'
    1.87 +      Seq.single st'
    1.88    end;
    1.89  
    1.90  (*Introduce a list of lemmas and subgoals*)
    1.91 @@ -496,7 +496,7 @@
    1.92  (*** Meta-Rewriting Tactics ***)
    1.93  
    1.94  fun result1 tacf mss thm =
    1.95 -  apsome fst (Sequence.pull (tacf mss thm));
    1.96 +  apsome fst (Seq.pull (tacf mss thm));
    1.97  
    1.98  val simple_prover =
    1.99    result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));