# HG changeset patch
# User sultana
# Date 1334701360 -3600
# Node ID 832ca5c3f1b1de138481411c2f9ca040fdde672c
# Parent  9c8a1b9c0630220eaaccc2ded7628b3b5345a2c7
updated TPTP's ROOT.ML to include TPTP_Interpret;

diff -r 9c8a1b9c0630 -r 832ca5c3f1b1 src/HOL/TPTP/ROOT.ML
--- a/src/HOL/TPTP/ROOT.ML	Tue Apr 17 23:24:46 2012 +0200
+++ b/src/HOL/TPTP/ROOT.ML	Tue Apr 17 23:22:40 2012 +0100
@@ -8,7 +8,7 @@
 
 use_thys [
   "ATP_Theory_Export",
-  "TPTP_Parser"
+  "TPTP_Interpret"
 ];
 
 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)