--- a/src/HOL/HOL.thy Wed Oct 19 08:37:15 2011 +0200
+++ b/src/HOL/HOL.thy Wed Oct 19 08:37:16 2011 +0200
@@ -28,7 +28,6 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induction.ML")
("~~/src/Tools/induct_tacs.ML")
- ("Tools/recfun_codegen.ML")
("Tools/cnf_funcs.ML")
"~~/src/Tools/subtyping.ML"
"~~/src/Tools/case_product.ML"
@@ -1715,66 +1714,6 @@
subsection {* Code generator setup *}
-subsubsection {* SML code generator setup *}
-
-use "Tools/recfun_codegen.ML"
-
-setup {*
- Codegen.setup
- #> RecfunCodegen.setup
- #> Codegen.map_unfold (K HOL_basic_ss)
-*}
-
-types_code
- "bool" ("bool")
-attach (term_of) {*
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-*}
-attach (test) {*
-fun gen_bool i =
- let val b = one_of [false, true]
- in (b, fn () => term_of_bool b) end;
-*}
- "prop" ("bool")
-attach (term_of) {*
-fun term_of_prop b =
- HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
-*}
-
-consts_code
- "Trueprop" ("(_)")
- "True" ("true")
- "False" ("false")
- "Not" ("Bool.not")
- HOL.disj ("(_ orelse/ _)")
- HOL.conj ("(_ andalso/ _)")
- "If" ("(if _/ then _/ else _)")
-
-setup {*
-let
-
-fun eq_codegen thy mode defs dep thyname b t gr =
- (case strip_comb t of
- (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const (@{const_name HOL.eq}, _), [t, u]) =>
- let
- val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
- val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
- val (_, gr''') =
- Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
- in
- SOME (Codegen.parens
- (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
- end
- | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
- thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
- | _ => NONE);
-
-in
- Codegen.add_codegen "eq_codegen" eq_codegen
-end
-*}
-
subsubsection {* Generic code generator preprocessor setup *}
setup {*
@@ -1979,10 +1918,6 @@
Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
*} "solve goal by evaluation"
-method_setup evaluation = {*
- Scan.succeed (gen_eval_method Codegen.evaluation_conv)
-*} "solve goal by evaluation"
-
method_setup normalization = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD'
(CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))