--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jan 04 23:22:53 2019 +0100
@@ -14,8 +14,8 @@
struct
val rews =
- map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o Logic.dest_equals o
- Logic.varify_global o Proof_Syntax.read_term @{theory} true propT o Syntax.implode_input)
+ map (apply2 (Proof_Syntax.proof_of_term \<^theory> true) o Logic.dest_equals o
+ Logic.varify_global o Proof_Syntax.read_term \<^theory> true propT o Syntax.implode_input)
(** eliminate meta-equality rules **)