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