src/Tools/Code/code_thingol.ML
changeset 35299 4f4d5bf4ea08
parent 35226 b987b803616d
child 35845 e5980f0ad025
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Feb 22 10:28:49 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Feb 22 11:10:20 2010 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4      | thyname :: _ => thyname;
     1.5    fun thyname_of_const thy c = case AxClass.class_of_param thy c
     1.6     of SOME class => thyname_of_class thy class
     1.7 -    | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
     1.8 +    | NONE => (case Code.get_type_of_constr_or_abstr thy c
     1.9         of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    1.10          | NONE => Codegen.thyname_of_const thy c);
    1.11    fun purify_base "==>" = "follows"
    1.12 @@ -543,7 +543,7 @@
    1.13    let
    1.14      val stmt_datatype =
    1.15        let
    1.16 -        val (vs, cos) = Code.get_datatype thy tyco;
    1.17 +        val (vs, cos) = Code.get_type thy tyco;
    1.18        in
    1.19          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.20          ##>> fold_map (fn (c, tys) =>
    1.21 @@ -569,7 +569,7 @@
    1.22          ##>> fold_map (translate_eqn thy algbr eqngr) eqns
    1.23          #>> (fn info => Fun (c, info))
    1.24        end;
    1.25 -    val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
    1.26 +    val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    1.27       of SOME (tyco, _) => stmt_datatypecons tyco
    1.28        | NONE => (case AxClass.class_of_param thy c
    1.29           of SOME class => stmt_classparam class