src/ZF/ROOT.ML
changeset 4271 3a82492e70c5
parent 4262 e4113a682883
child 5511 7f52fb755581
     1.1 --- a/src/ZF/ROOT.ML	Fri Nov 21 15:27:43 1997 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Nov 21 15:29:56 1997 +0100
     1.3 @@ -15,11 +15,11 @@
     1.4  
     1.5  (*For Pure/tactic??  A crude way of adding structure to rules*)
     1.6  fun CHECK_SOLVED tac st =
     1.7 -    case Sequence.pull (tac st) of
     1.8 +    case Seq.pull (tac st) of
     1.9          None => error"DO_GOAL: tactic list failed"
    1.10        | Some(x,_) => 
    1.11                  if has_fewer_prems 1 x then
    1.12 -                    Sequence.cons(x, Sequence.null)
    1.13 +                    Seq.cons(x, Seq.empty)
    1.14                  else (writeln"DO_GOAL: unsolved goals!!";
    1.15                        writeln"Final proof state was ...";
    1.16                        print_goals (!goals_limit) x;