# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID 7c78f14d20cffae170cd470336b35dc4f573126c
# Parent  e699f754d9f723fc74832b9c8d0ef72d12bfc52d
cleaner handling of metacharacters + freshness of one-off facts

diff -r e699f754d9f7 -r 7c78f14d20cf src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -18,17 +18,6 @@
 
 open Sledgehammer_Filter_MaSh
 
-val unescape_meta =
-  let
-    fun un accum [] = String.implode (rev accum)
-      | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
-        (case Int.fromString (String.implode [d1, d2, d3]) of
-           SOME n => un (Char.chr n :: accum) cs
-         | NONE => "" (* error *))
-      | un _ (#"\\" :: _) = "" (* error *)
-      | un accum (c :: cs) = un (c :: accum) cs
-  in un [] o String.explode end
-
 val isarN = "Isa"
 val iterN = "Iter"
 val mashN = "MaSh"