1.1 --- a/src/Tools/code/code_funcgr.ML	Mon May 26 17:55:37 2008 +0200
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Mon May 26 17:55:38 2008 +0200
     1.3 @@ -88,8 +88,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -exception CLASS_ERROR of string list * string;
     1.8 -
     1.9  fun resort_thms thy algebra typ_of thms =
    1.10    let
    1.11      val cs = fold_consts (insert (op =)) thms [];
    1.12 @@ -104,13 +102,14 @@
    1.13    let
    1.14      val typ_funcgr = try (fst o Graph.get_node funcgr);
    1.15      val resort_dep = apsnd (resort_thms thy algebra typ_funcgr);
    1.16 -    fun resort_rec typ_of (const, []) = (true, (const, []))
    1.17 -      | resort_rec typ_of (const, thms as thm :: _) =
    1.18 -          let
    1.19 +    fun resort_rec typ_of (c, []) = (true, (c, []))
    1.20 +      | resort_rec typ_of (c, thms as thm :: _) = if is_some (AxClass.inst_of_param thy c)
    1.21 +          then (true, (c, thms))
    1.22 +          else let
    1.23              val (_, (vs, ty)) = CodeUnit.head_func thm;
    1.24              val thms' as thm' :: _ = resort_thms thy algebra typ_of thms
    1.25              val (_, (vs', ty')) = CodeUnit.head_func thm'; (*FIXME simplify check*)
    1.26 -          in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
    1.27 +          in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
    1.28      fun resort_recs funcss =
    1.29        let
    1.30          fun typ_of c = case these (AList.lookup (op =) funcss c)
    1.31 @@ -184,19 +183,7 @@
    1.32        |> resort_funcss thy algebra funcgr
    1.33        |> filter_out (can (Graph.get_node funcgr) o fst);
    1.34      fun typ_func c [] = Code.default_typ thy c
    1.35 -      | typ_func c (thms as thm :: _) = case AxClass.inst_of_param thy c
    1.36 -         of SOME (c', tyco) => 
    1.37 -              let
    1.38 -                val (_, (vs, ty)) = CodeUnit.head_func thm;
    1.39 -                val SOME class = AxClass.class_of_param thy c';
    1.40 -                val sorts_decl = Sorts.mg_domain algebra tyco [class];
    1.41 -              in if map snd vs = sorts_decl then (vs, ty)
    1.42 -                else raise CLASS_ERROR ([c], "Illegal instantation for class operation "
    1.43 -                  ^ CodeUnit.string_of_const thy c
    1.44 -                  ^ "\nin defining equations\n"
    1.45 -                  ^ (cat_lines o map (Display.string_of_thm o AxClass.overload thy)) thms)
    1.46 -              end
    1.47 -          | NONE => (snd o CodeUnit.head_func) thm;
    1.48 +      | typ_func c (thms as thm :: _) = (snd o CodeUnit.head_func) thm;
    1.49      fun add_funcs (const, thms) =
    1.50        Graph.new_node (const, (typ_func const thms, thms));
    1.51      fun add_deps (funcs as (const, thms)) funcgr =
    1.52 @@ -206,7 +193,7 @@
    1.53            (fold_consts (insert (op =)) thms []);
    1.54        in
    1.55          funcgr
    1.56 -        |> ensure_consts' thy algebra insts
    1.57 +        |> ensure_consts thy algebra insts
    1.58          |> fold (curry Graph.add_edge const) deps
    1.59          |> fold (curry Graph.add_edge const) insts
    1.60         end;
    1.61 @@ -215,7 +202,7 @@
    1.62      |> fold add_funcs funcss
    1.63      |> fold add_deps funcss
    1.64    end
    1.65 -and ensure_consts' thy algebra cs funcgr =
    1.66 +and ensure_consts thy algebra cs funcgr =
    1.67    let
    1.68      val auxgr = Graph.empty
    1.69        |> fold (snd oo ensure_const thy algebra funcgr) cs;
    1.70 @@ -224,26 +211,19 @@
    1.71      |> fold (merge_funcss thy algebra)
    1.72           (map (AList.make (Graph.get_node auxgr))
    1.73           (rev (Graph.strong_conn auxgr)))
    1.74 -  end handle CLASS_ERROR (cs', msg)
    1.75 -    => raise CLASS_ERROR (fold (insert (op =)) cs' cs, msg);
    1.76 +  end;
    1.77  
    1.78  in
    1.79  
    1.80  (** retrieval interfaces **)
    1.81  
    1.82 -fun ensure_consts thy algebra consts funcgr =
    1.83 -  ensure_consts' thy algebra consts funcgr
    1.84 -    handle CLASS_ERROR (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
    1.85 -    ^ commas (map (CodeUnit.string_of_const thy) cs'));
    1.86 +val ensure_consts = ensure_consts;
    1.87  
    1.88  fun check_consts thy consts funcgr =
    1.89    let
    1.90      val algebra = Code.coregular_algebra thy;
    1.91 -    fun try_const const funcgr =
    1.92 -      (SOME const, ensure_consts' thy algebra [const] funcgr)
    1.93 -      handle CLASS_ERROR (cs', msg) => (NONE, funcgr);
    1.94 -    val (consts', funcgr') = fold_map try_const consts funcgr;
    1.95 -  in (map_filter I consts', funcgr') end;
    1.96 +    fun try_const const funcgr = (const, ensure_consts thy algebra [const] funcgr);
    1.97 +  in fold_map try_const consts funcgr end;
    1.98  
    1.99  fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
   1.100    let