better error reporting
authorhaftmann
Tue Jan 08 11:37:29 2008 +0100 (2008-01-08 ago)
changeset 258635b4a8b1d0f88
parent 25862 9756a80d8a13
child 25864 11f531354852
better error reporting
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Jan 08 11:37:28 2008 +0100
     1.2 +++ b/src/Pure/axclass.ML	Tue Jan 08 11:37:29 2008 +0100
     1.3 @@ -201,7 +201,7 @@
     1.4  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
     1.5    (get_inst_params thy) [];
     1.6  
     1.7 -val inst_tyco_of = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
     1.8 +fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
     1.9  
    1.10  fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    1.11  fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));