src/HOL/Tools/code_evaluation.ML
changeset 40726 16dcfedc4eb7
parent 39567 5ee997fbe5cc
child 41184 5c6f44d22f51
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri Nov 26 18:07:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Nov 26 22:33:21 2010 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  (* code equations for datatypes *)
     1.6  
     1.7 -fun mk_term_of_eq thy ty (c, tys) =
     1.8 +fun mk_term_of_eq thy ty (c, (_, tys)) =
     1.9    let
    1.10      val t = list_comb (Const (c, tys ---> ty),
    1.11        map Free (Name.names Name.context "a" tys));
    1.12 @@ -74,7 +74,7 @@
    1.13      val vs = map (fn (v, sort) =>
    1.14        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    1.15      val ty = Type (tyco, map TFree vs);
    1.16 -    val cs = (map o apsnd o map o map_atyps)
    1.17 +    val cs = (map o apsnd o apsnd o map o map_atyps)
    1.18        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.19      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.20      val eqs = map (mk_term_of_eq thy ty) cs;
    1.21 @@ -121,7 +121,7 @@
    1.22      |> Code.add_eqn eq
    1.23    end;
    1.24  
    1.25 -fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
    1.26 +fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
    1.27    let
    1.28      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.29    in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;