src/HOLCF/domain/theorems.ML
changeset 4271 3a82492e70c5
parent 4252 d5ccc8321e1e
child 4721 c8a8482a8124
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Nov 21 15:27:43 1997 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Nov 21 15:29:56 1997 +0100
     1.3 @@ -28,9 +28,9 @@
     1.4                                  | prems=> (cut_facts_tac prems 1)::tacsf);
     1.5  
     1.6  fun REPEAT_DETERM_UNTIL p tac = 
     1.7 -let fun drep st = if p st then Sequence.single st
     1.8 -                          else (case Sequence.pull(tac st) of
     1.9 -                                  None        => Sequence.null
    1.10 +let fun drep st = if p st then Seq.single st
    1.11 +                          else (case Seq.pull(tac st) of
    1.12 +                                  None        => Seq.empty
    1.13                                  | Some(st',_) => drep st')
    1.14  in drep end;
    1.15  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);