# HG changeset patch # User Cezary Kaliszyk # 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;