# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271152445 -7200
# Node ID 890e60829e59e7713aced0ef94426806bb7e58cc
# Parent  6e600c7f0274d96820b2bbe61e9397576b5dd0bd# Parent  45f8898fe4cfa82b92c11c22128c336078ac521b
merge

diff -r 6e600c7f0274 -r 890e60829e59 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Apr 13 11:40:55 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Apr 13 11:54:05 2010 +0200
@@ -423,7 +423,7 @@
 
 fun get_abstype_spec thy tyco = case get_type_entry thy tyco
  of SOME (vs, Abstractor spec) => (vs, spec)
-  | NONE => error ("Not an abstract type: " ^ tyco);
+  | _ => error ("Not an abstract type: " ^ tyco);
  
 fun get_type thy = fst o get_type_spec thy;