src/Pure/axclass.ML
changeset 32791 e6d47ce70d27
parent 32765 3032c0308019
child 32966 5b21661fe618
     1.1 --- a/src/Pure/axclass.ML	Wed Sep 30 22:31:16 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Sep 30 22:53:33 2009 +0200
     1.3 @@ -150,7 +150,6 @@
     1.4    let val params = #2 (get_axclasses thy);
     1.5    in fold (fn (x, c) => if pred c then cons x else I) params [] end;
     1.6  
     1.7 -fun params_of thy c = get_params thy (fn c' => c' = c);
     1.8  fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
     1.9  
    1.10  fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
    1.11 @@ -263,7 +262,8 @@
    1.12  
    1.13  fun unoverload_const thy (c_ty as (c, _)) =
    1.14    case class_of_param thy c
    1.15 -   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
    1.16 +   of SOME class (* FIXME unused? *) =>
    1.17 +     (case get_inst_tyco (Sign.consts_of thy) c_ty
    1.18         of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    1.19          | NONE => c)
    1.20      | NONE => c;
    1.21 @@ -585,7 +585,7 @@
    1.22          val hyps = vars
    1.23            |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
    1.24          val ths = (typ, sort)
    1.25 -          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
    1.26 +          |> Sorts.of_sort_derivation (Sign.classes_of thy)
    1.27             {class_relation =
    1.28                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    1.29              type_constructor =