equal
deleted
inserted
replaced
1956 (Scala "!error(\"undefined\")") |
1956 (Scala "!error(\"undefined\")") |
1957 |
1957 |
1958 subsubsection {* Evaluation and normalization by evaluation *} |
1958 subsubsection {* Evaluation and normalization by evaluation *} |
1959 |
1959 |
1960 setup {* |
1960 setup {* |
1961 Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) |
1961 Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) (* FIXME proper context!? *) |
1962 *} |
1962 *} |
1963 |
1963 |
1964 ML {* |
1964 ML {* |
1965 fun gen_eval_method conv ctxt = SIMPLE_METHOD' |
1965 fun gen_eval_method conv ctxt = SIMPLE_METHOD' |
1966 (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (ProofContext.theory_of ctxt)))) ctxt) |
1966 (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (ProofContext.theory_of ctxt)))) ctxt) |