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.
better error reporting
authorhaftmann
Tue, 08 Jan 2008 11:37:29 +0100
changeset 25863 5b4a8b1d0f88
parent 25862 9756a80d8a13
child 25864 11f531354852
better error reporting
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Tue Jan 08 11:37:28 2008 +0100
+++ b/src/Pure/axclass.ML	Tue Jan 08 11:37:29 2008 +0100
@@ -201,7 +201,7 @@
 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   (get_inst_params thy) [];
 
-val inst_tyco_of = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
+fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
 
 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
isabelle