src/HOL/Code_Eval.thy
changeset 31746 75fe3304015c
parent 31594 a94aa5f045fb
child 31998 2c7a24f74db9
equal deleted inserted replaced
31744:dc3c2d52b642 31746:75fe3304015c
    83       |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    83       |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    84       |> Thm.varifyT
    84       |> Thm.varifyT
    85     end;
    85     end;
    86   fun add_term_of_code tyco raw_vs raw_cs thy =
    86   fun add_term_of_code tyco raw_vs raw_cs thy =
    87     let
    87     let
    88       val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    88       val algebra = Sign.classes_of thy;
       
    89       val vs = map (fn (v, sort) =>
       
    90         (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    89       val ty = Type (tyco, map TFree vs);
    91       val ty = Type (tyco, map TFree vs);
    90       val cs = (map o apsnd o map o map_atyps)
    92       val cs = (map o apsnd o map o map_atyps)
    91         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    93         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    92       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    94       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    93       val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
    95       val eqs = map (mk_term_of_eq thy ty vs tyco) cs;