# HG changeset patch
# User haftmann
# Date 1271151012 -7200
# Node ID 45f8898fe4cfa82b92c11c22128c336078ac521b
# Parent  86b952fc31dab8bd963895c00b6118f4475e490f
more accurate pattern match

diff -r 86b952fc31da -r 45f8898fe4cf src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Apr 13 11:13:52 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Apr 13 11:30:12 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;