src/ZF/ROOT.ML
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/ROOT.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -12,9 +12,8 @@
     1.4  writeln banner;
     1.5  
     1.6  (*For Pure/tactic??  A crude way of adding structure to rules*)
     1.7 -fun CHECK_SOLVED (Tactic tf) = 
     1.8 -  Tactic (fn state => 
     1.9 -    case Sequence.pull (tf state) of
    1.10 +fun CHECK_SOLVED tac st =
    1.11 +    case Sequence.pull (tac st) of
    1.12          None => error"DO_GOAL: tactic list failed"
    1.13        | Some(x,_) => 
    1.14                  if has_fewer_prems 1 x then
    1.15 @@ -22,7 +21,7 @@
    1.16                  else (writeln"DO_GOAL: unsolved goals!!";
    1.17                        writeln"Final proof state was ...";
    1.18                        print_goals (!goals_limit) x;
    1.19 -                      raise ERROR));
    1.20 +                      raise ERROR);
    1.21  
    1.22  fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    1.23