src/HOL/Transitive_Closure.thy
changeset 15531 08c8dad8e399
parent 15140 322485b816ac
child 15551 af78481b37bf
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -470,8 +470,8 @@
     1.4  	      | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
     1.5  	      | decr r = (r,"r");
     1.6  	    val (rel,r) = decr rel;
     1.7 -	in Some (a,b,rel,r) end
     1.8 -      | dec _ =  None 
     1.9 +	in SOME (a,b,rel,r) end
    1.10 +      | dec _ =  NONE 
    1.11      in dec t end;
    1.12    
    1.13    end); (* struct *)