src/HOLCF/domain/theorems.ML
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1637 b8a8ae2e5de1
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -46,10 +46,10 @@
     1.4  
     1.5  fun REPEAT_DETERM_UNTIL p tac = 
     1.6  let fun drep st = if p st then Sequence.single st
     1.7 -                          else (case Sequence.pull(tapply(tac,st)) of
     1.8 +                          else (case Sequence.pull(tac st) of
     1.9                                    None        => Sequence.null
    1.10                                  | Some(st',_) => drep st')
    1.11 -in Tactic drep end;
    1.12 +in drep end;
    1.13  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
    1.14  
    1.15  local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in