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 *)