# HG changeset patch
# User blanchet
# Date 1342593843 -7200
# Node ID a3cb8901d60cb023ded911d351f6ab04f3abbd01
# Parent  8a1ef12f7e6da19f8178e473922da6b1f9d38f69
clean up dependencies

diff -r 8a1ef12f7e6d -r a3cb8901d60c src/HOL/TPTP/MaSh_Import.thy
--- a/src/HOL/TPTP/MaSh_Import.thy	Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -9,6 +9,10 @@
 uses "mash_import.ML"
 begin
 
+sledgehammer_params
+  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
diff -r 8a1ef12f7e6d -r a3cb8901d60c src/HOL/TPTP/ROOT.ML
--- a/src/HOL/TPTP/ROOT.ML	Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/ROOT.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -7,6 +7,8 @@
 *)
 
 use_thys [
+  "ATP_Theory_Export",
+  "MaSh_Export",
   "MaSh_Import",
   "TPTP_Interpret",
   "THF_Arith"
diff -r 8a1ef12f7e6d -r a3cb8901d60c src/HOL/TPTP/mash_import.ML
--- a/src/HOL/TPTP/mash_import.ML	Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -18,7 +18,6 @@
 struct
 
 open Sledgehammer_Filter_MaSh
-open MaSh_Export
 
 val unescape_meta =
   let