src/HOL/ex/Predicate_Compile.thy
changeset 31225 df6945ac4193
parent 31217 c025f32afd4e
child 32308 c2b74affab85
child 32340 b4632820e74c
equal deleted inserted replaced
31224:6f4fb815439a 31225:df6945ac4193
    22     fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
    22     fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
    23     val T1 = T --> @{typ term};
    23     val T1 = T --> @{typ term};
    24     val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
    24     val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
    25     val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
    25     val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
    26       $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
    26       $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
    27   in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) @{code Predicate.map} thy t' []) end;
    27   in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
    28 
    28 
    29 fun values ctxt k t_compr =
    29 fun values ctxt k t_compr =
    30   let
    30   let
    31     val thy = ProofContext.theory_of ctxt;
    31     val thy = ProofContext.theory_of ctxt;
    32     val (T, t') = eval thy t_compr;
    32     val (T, t') = eval thy t_compr;