# HG changeset patch
# User haftmann
# Date 1292606684 -3600
# Node ID c5cb19ecbd419535a1d777188cf3dcb7f04d0e12
# Parent  e1da70df68c16bb5427301ea857092df2b687c14
avoid slightly odd Conv.tap_thy

diff -r e1da70df68c1 -r c5cb19ecbd41 src/HOL/HOL.thy
--- 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"
 
 
diff -r e1da70df68c1 -r c5cb19ecbd41 src/HOL/Tools/code_evaluation.ML
--- 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
diff -r e1da70df68c1 -r c5cb19ecbd41 src/Tools/Code/code_runtime.ML
--- 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
diff -r e1da70df68c1 -r c5cb19ecbd41 src/Tools/Code/code_simp.ML
--- 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)))
diff -r e1da70df68c1 -r c5cb19ecbd41 src/Tools/nbe.ML
--- 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