src/HOLCF/domain/theorems.ML
changeset 1638 69c094639823
parent 1637 b8a8ae2e5de1
child 1644 681f70ca3cf7
--- a/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:27:14 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Apr 03 20:08:27 1996 +0200
@@ -1,4 +1,4 @@
-(* theorems.ML
+ (* theorems.ML
    Author : David von Oheimb
    Created: 06-Jun-95
    Updated: 08-Jun-95 first proof from cterms
@@ -39,10 +39,10 @@
 
 fun REPEAT_DETERM_UNTIL p tac = 
 let fun drep st = if p st then Sequence.single st
-			  else (case Sequence.pull(tapply(tac,st)) of
+			  else (case Sequence.pull(tac st) of
 		                  None        => Sequence.null
 				| Some(st',_) => drep st')
-in Tactic drep end;
+in drep end;
 val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
 
 local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in