| changeset 69597 | ff784d5a5bfb |
| parent 63167 | 0909deb8059b |
| child 69605 | a96320074298 |
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Sat Jan 05 17:24:33 2019 +0100 @@ -17,8 +17,8 @@ ML \<open> val do_it = false (* switch to "true" to generate the files *) -val ctxt = @{context} -val thy = @{theory Complex_Main} +val ctxt = \<^context> +val thy = \<^theory>\<open>Complex_Main\<close> val infer_policy = (* Unchecked_Inferences *) No_Inferences \<close>