# HG changeset patch
# User oheimb
# Date 828554907 -7200
# Node ID 69c0946398237a3bd73abdcee59566139bb415b8
# Parent  b8a8ae2e5de1ff627087b2b028eee45f83302768
*** empty log message ***

diff -r b8a8ae2e5de1 -r 69c094639823 src/HOLCF/domain/theorems.ML
--- 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