--- a/src/HOL/HoareParallel/OG_Syntax.thy Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/HoareParallel/OG_Syntax.thy Sun Feb 13 17:15:14 2005 +0100
@@ -96,8 +96,8 @@
fun upd_tr' (x_upd, T) =
(case try (unsuffix RecordPackage.updateN) x_upd of
- Some x => (x, if T = dummyT then T else Term.domain_type T)
- | None => raise Match);
+ SOME x => (x, if T = dummyT then T else Term.domain_type T)
+ | NONE => raise Match);
fun update_name_tr' (Free x) = Free (upd_tr' x)
| update_name_tr' ((c as Const ("_free", _)) $ Free x) =