From f8bcd2557c5f87ba145c28dbbdeb9716406d695f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 9 Mar 2019 21:13:04 +0000 Subject: [PATCH] Removed call to obsolete unquote_string. --- Isa_DOF.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 5068f01..b581aeb 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -878,7 +878,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = | ltx_of_term ctxt t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s))) fun ltx_of_markup s = let - val old_str = unquote_string (markup2string s) + val old_str = (markup2string s) val ctxt = Proof_Context.init_global thy val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s val str_of_term = ltx_of_term ctxt term