# HG changeset patch
# User haftmann
# Date 1487792064 -3600
# Node ID fd753468786f5cb649ff721d70f8751be26c9226
# Parent  956ea00a162aea5308c66829c84d360a00fe32dc
explicit dynamic context for gap-bridging function

diff -r 956ea00a162a -r fd753468786f src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Wed Feb 22 20:33:53 2017 +0100
+++ b/src/Doc/Codegen/Computations.thy	Wed Feb 22 20:34:24 2017 +0100
@@ -286,7 +286,7 @@
     "minus :: int \<Rightarrow> int \<Rightarrow> int"
     "times :: int \<Rightarrow> int \<Rightarrow> int"
     "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
-  } (curry dvd_oracle)
+  } (K (curry dvd_oracle))
 
   end
 \<close>
@@ -345,15 +345,15 @@
 
   val divisor = Thm.dest_arg o Thm.dest_arg;
 
-  fun evaluate thm = 
-    Simplifier.rewrite_rule 
-      (Proof_Context.transfer (Thm.theory_of_thm thm) @{context})
-      (map mk_eq @{thms arith_simps positive_mult}) thm; (*FIXME proper ctxt*)
+  val evaluate_simps = map mk_eq @{thms arith_simps positive_mult};
 
-  fun revaluate k ct =
+  fun evaluate ctxt = 
+    Simplifier.rewrite_rule ctxt evaluate_simps;
+
+  fun revaluate ctxt k ct =
     @{thm conv_div_cert}
     |> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
-    |> evaluate;
+    |> evaluate ctxt;
 
   in
 
diff -r 956ea00a162a -r fd753468786f src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Feb 22 20:33:53 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Feb 22 20:34:24 2017 +0100
@@ -682,7 +682,7 @@
       "0::nat" "1::nat" "2::nat" "3::nat"
       "0::int" "1::int" "2::int" "3::int" "-1::int"
   datatypes: polex "(polex * polex) list" int integer num}
-  (fn p => fn ct => pol_oracle @{context} ct (term_of_pol p))
+  (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p))
 
 end
 \<close>
diff -r 956ea00a162a -r fd753468786f src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Feb 22 20:33:53 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Feb 22 20:34:24 2017 +0100
@@ -675,7 +675,7 @@
     "0::nat" "1::nat" "2::nat" "3::nat"
     "0::int" "1::int" "2::int" "3::int" "-1::int"
   datatypes: fexpr int integer num}
-  (fn result => fn ct => fnorm_oracle @{context} ct (term_of_result result))
+  (fn ctxt => fn result => fn ct => fnorm_oracle ctxt ct (term_of_result result))
 
 end
 \<close>
diff -r 956ea00a162a -r fd753468786f src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Feb 22 20:33:53 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Feb 22 20:34:24 2017 +0100
@@ -35,7 +35,7 @@
   val mount_computation: Proof.context -> (string * typ) list -> typ
     -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
   val mount_computation_conv: Proof.context -> (string * typ) list -> typ
-    -> (term -> 'ml) -> ('ml -> conv) -> Proof.context -> conv
+    -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv
   val mount_computation_check: Proof.context -> (string * typ) list
     -> (term -> truth) -> Proof.context -> conv
   val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
@@ -435,7 +435,7 @@
       { ctxt = ctxt, consts = [] }
       (K (fn ctxt' => fn t =>
         case checked_computation cTs raw_computation ctxt' t of
-          SOME x => conv x
+          SOME x => conv ctxt' x
         | NONE => Conv.all_conv)));
   in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end;
 
@@ -451,7 +451,7 @@
 
 fun mount_computation_check ctxt cTs raw_computation =
   mount_computation_conv ctxt cTs @{typ prop} raw_computation
-    (K holds_oracle);
+    ((K o K) holds_oracle);
 
 end;