src/Pure/axclass.ML
changeset 25863 5b4a8b1d0f88
parent 25617 b495384e48e1
child 26246 e212c22f35c2
     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));