more accurate pattern match
authorhaftmann
Tue, 13 Apr 2010 11:30:12 +0200
changeset 36122 45f8898fe4cf
parent 36121 86b952fc31da
child 36125 890e60829e59
more accurate pattern match
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;