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