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>