src/HOL/ex/SVC_Oracle.ML

--- a/src/HOL/ex/SVC_Oracle.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -39,8 +39,8 @@
 	    Free _  => t  (*but not existing Vars, lest the names clash*)
 	  | Bound _ => t
 	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
-		      Some v => v
-		    | None   => insert t)
+		      SOME v => v
+		    | NONE   => insert t)
     (*abstraction of a numeric literal*)
     fun lit (t as Const("0", _)) = t
       | lit (t as Const("1", _)) = t