src/HOL/Library/Eval.thy
changeset 24621 97d403d9ab54
parent 24587 4f2cbf6e563f
child 24626 85eceef2edc7
equal deleted inserted replaced
24620:40811901b998 24621:97d403d9ab54
    53       (Type (tyco,
    53       (Type (tyco,
    54         map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
    54         map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
    55   fun hook specs =
    55   fun hook specs =
    56     DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    56     DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    57       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    57       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    58       [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
    58       [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
    59 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    59 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    60 *}
    60 *}
    61 
    61 
    62 
    62 
    63 subsection {* @{text term_of} class *}
    63 subsection {* @{text term_of} class *}
   174 {* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
   174 {* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
   175 let
   175 let
   176   val _ = (Term.map_types o Term.map_atyps) (fn _ =>
   176   val _ = (Term.map_types o Term.map_atyps) (fn _ =>
   177     error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
   177     error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
   178     t0;
   178     t0;
   179 in Logic.mk_equals (t0, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end;
   179 in
       
   180   Logic.mk_equals (t0,
       
   181     CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
       
   182 end;
   180 *}
   183 *}
   181 
   184 
   182 ML {*
   185 ML {*
   183 structure Eval : EVAL =
   186 structure Eval : EVAL =
   184 struct
   187 struct