Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 13 Apr 2010 11:54:05 +0200
changeset 36125 890e60829e59
parent 36124 6e600c7f0274 (current diff)
parent 36122 45f8898fe4cf (diff)
child 36129 186fcdb8d00f
merge
--- 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;
isabelle