--- a/src/HOL/HOL.thy Fri Dec 17 18:24:44 2010 +0100
+++ b/src/HOL/HOL.thy Fri Dec 17 18:24:44 2010 +0100
@@ -1964,19 +1964,20 @@
ML {*
fun gen_eval_method conv ctxt = SIMPLE_METHOD'
- (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
+ (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (ProofContext.theory_of ctxt)))) ctxt)
THEN' rtac TrueI)
*}
method_setup eval = {* Scan.succeed (gen_eval_method Code_Runtime.dynamic_holds_conv) *}
"solve goal by evaluation"
-method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
+method_setup evaluation = {* Scan.succeed (gen_eval_method (K Codegen.evaluation_conv)) *}
"solve goal by evaluation"
method_setup normalization = {*
- Scan.succeed (K (SIMPLE_METHOD'
- (CHANGED_PROP o (CONVERSION Nbe.dynamic_conv THEN' (fn k => TRY (rtac TrueI k))))))
+ Scan.succeed (fn ctxt => SIMPLE_METHOD'
+ (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (ProofContext.theory_of ctxt))
+ THEN' (fn k => TRY (rtac TrueI k)))))
*} "solve goal by normalization"
--- a/src/HOL/Tools/code_evaluation.ML Fri Dec 17 18:24:44 2010 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Fri Dec 17 18:24:44 2010 +0100
@@ -12,7 +12,7 @@
val static_value: theory -> string list -> typ list -> term -> term option
val static_value_strict: theory -> string list -> typ list -> term -> term
val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
- val dynamic_conv: conv
+ val dynamic_conv: theory -> conv
val static_conv: theory -> string list -> typ list -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
@@ -194,8 +194,8 @@
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
end;
-val dynamic_conv = Conv.tap_thy
- (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
+fun dynamic_conv thy = certify_eval thy (dynamic_value thy)
+ (Code_Runtime.dynamic_holds_conv thy);
fun static_conv thy consts Ts =
let
--- a/src/Tools/Code/code_runtime.ML Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Dec 17 18:24:44 2010 +0100
@@ -23,7 +23,7 @@
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
val static_value_exn: 'a cookie -> theory -> string option
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
- val dynamic_holds_conv: conv
+ val dynamic_holds_conv: theory -> conv
val static_holds_conv: theory -> string list -> conv
val code_reflect: (string * string list option) list -> string list -> string
-> string option -> theory -> theory
@@ -175,9 +175,9 @@
fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
-val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
- (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
- o reject_vars thy);
+fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
+ (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
+ o reject_vars thy;
fun static_holds_conv thy consts =
let
--- a/src/Tools/Code/code_simp.ML Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Fri Dec 17 18:24:44 2010 +0100
@@ -7,7 +7,7 @@
signature CODE_SIMP =
sig
val map_ss: (simpset -> simpset) -> theory -> theory
- val dynamic_conv: conv
+ val dynamic_conv: theory -> conv
val dynamic_tac: theory -> int -> tactic
val dynamic_value: theory -> term -> term
val static_conv: theory -> simpset option -> string list -> conv
@@ -51,12 +51,12 @@
(* evaluation with dynamic code context *)
-val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
- (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
+fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
+ (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program);
-fun dynamic_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
+fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
-fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy;
+fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
val setup = Method.setup (Binding.name "code_simp")
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of)))
--- a/src/Tools/nbe.ML Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/nbe.ML Fri Dec 17 18:24:44 2010 +0100
@@ -6,7 +6,7 @@
signature NBE =
sig
- val dynamic_conv: conv
+ val dynamic_conv: theory -> conv
val dynamic_value: theory -> term -> term
val static_conv: theory -> string list -> conv
val static_value: theory -> string list -> term -> term
@@ -593,9 +593,8 @@
fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-val dynamic_conv = Conv.tap_thy (fn thy =>
- lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
- (K (fn program => oracle thy program (compile false thy program)))));
+fun dynamic_conv thy = lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
+ (K (fn program => oracle thy program (compile false thy program))));
fun dynamic_value thy = lift_triv_classes_rew thy
(Code_Thingol.dynamic_value thy I