changeset 65043 | fd753468786f |
parent 64999 | f8f76a501d25 |
child 67123 | 3fe40ff1b921 |
--- 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>