# HG changeset patch
# User haftmann
# Date 1199788649 -3600
# Node ID 5b4a8b1d0f88ae5e88e704145d301b0cc0d0f25c
# Parent  9756a80d8a136542ecec1d3ece41c864209fa45d
better error reporting

diff -r 9756a80d8a13 -r 5b4a8b1d0f88 src/Pure/axclass.ML
--- 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));