--- a/src/HOL/Orderings.thy Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Orderings.thy Sun Feb 13 17:15:14 2005 +0100
@@ -290,21 +290,21 @@
let fun of_sort t = Sign.of_sort sign (type_of t, sort)
fun dec (Const ("Not", _) $ t) = (
case dec t of
- None => None
- | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
+ NONE => NONE
+ | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
| dec (Const ("op =", _) $ t1 $ t2) =
if of_sort t1
- then Some (t1, "=", t2)
- else None
+ then SOME (t1, "=", t2)
+ else NONE
| dec (Const ("op <=", _) $ t1 $ t2) =
if of_sort t1
- then Some (t1, "<=", t2)
- else None
+ then SOME (t1, "<=", t2)
+ else NONE
| dec (Const ("op <", _) $ t1 $ t2) =
if of_sort t1
- then Some (t1, "<", t2)
- else None
- | dec _ = None
+ then SOME (t1, "<", t2)
+ else NONE
+ | dec _ = NONE
in dec t end;
structure Quasi_Tac = Quasi_Tac_Fun (