1.1 --- a/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:38 2008 +0200
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:40 2008 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4        Sorts.of_sort_derivation (Sign.pp thy) algebra
     1.5          { class_relation = class_relation, type_constructor = type_constructor,
     1.6            type_variable = type_variable }
     1.7 -        (ty, sort)
     1.8 +        (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
     1.9    in
    1.10      flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
    1.11    end;
    1.12 @@ -110,20 +110,18 @@
    1.13          val thy = Thm.theory_of_thm thm;
    1.14          val pp = Sign.pp thy;
    1.15          val cs = fold_consts (insert (op =)) thms [];
    1.16 -        fun class_error (c, ty_decl) e =
    1.17 -          error ;
    1.18          fun match_const c (ty, ty_decl) =
    1.19            let
    1.20              val tys = Sign.const_typargs thy (c, ty);
    1.21              val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
    1.22 -          in fn tab => fold2 (Type.typ_of_sort algebra) tys sorts tab 
    1.23 +          in fn tab => fold2 (curry (Sorts.meet_sort algebra)) tys sorts tab
    1.24              handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.msg_class_error pp e ^ ",\n"
    1.25                ^ "for constant " ^ CodeUnit.string_of_const thy c
    1.26                ^ "\nin defining equations(s)\n"
    1.27                ^ (cat_lines o map string_of_thm) thms)
    1.28 +            (*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*)
    1.29            end;
    1.30 -        fun match (c, ty) =
    1.31 -          case tap_typ c
    1.32 +        fun match (c, ty) = case tap_typ c
    1.33             of SOME ty_decl => match_const c (ty, ty_decl)
    1.34              | NONE => I;
    1.35          val tvars = fold match cs Vartab.empty;
    1.36 @@ -161,7 +159,7 @@
    1.37      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
    1.38      fun all_classparams tyco class =
    1.39        these (try (#params o AxClass.get_info thy) class)
    1.40 -      |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
    1.41 +      |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
    1.42    in
    1.43      Symtab.empty
    1.44      |> fold (fn (tyco, class) =>
    1.45 @@ -173,7 +171,7 @@
    1.46  fun instances_of_consts thy algebra funcgr consts =
    1.47    let
    1.48      fun inst (cexpr as (c, ty)) = insts_of thy algebra c
    1.49 -      ((fst o Graph.get_node funcgr) c) ty handle Sorts.CLASS_ERROR _ => [];
    1.50 +      ((fst o Graph.get_node funcgr) c) ty;
    1.51    in
    1.52      []
    1.53      |> fold (fold (insert (op =)) o inst) consts