# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID 0a84dc31601fb17f73c556b53d9386e1a627d9f6
# Parent  8dc9dc241973151d78e6764889e72e15fae7c555
took out test driver

diff -r 8dc9dc241973 -r 0a84dc31601f src/HOL/TPTP/TPTP_Interpret.thy
--- a/src/HOL/TPTP/TPTP_Interpret.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -14,64 +14,4 @@
 
 ML_file "TPTP_Parser/tptp_interpret.ML"
 
-
-ML {*
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Problem_Generate
-open ATP_Systems
-
-fun exploded_absolute_path file_name =
-  Path.explode file_name
-  |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD"))
-
-fun read_tptp_file thy postproc file_name =
-  let
-    fun has_role role (_, role', _, _) = (role' = role)
-    fun get_prop f (name, _, P, _) =
-      let val P' = P |> f |> close_form in
-        (name, P') |> postproc
-      end
-    val path = exploded_absolute_path file_name
-    val ((_, _, problem), thy) =
-      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"]
-                                    path [] [] thy
-    val (conjs, defs_and_nondefs) =
-      problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
-              ||> List.partition (has_role TPTP_Syntax.Role_Definition)
-  in
-    (map (get_prop I) conjs,
-     pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
-     Proof_Context.init_global thy)
-  end
-*}
-
-declare [[ML_exception_trace]]
-
-setup {*
-snd o Theory.specify_const ((@{binding c}, @{typ "'b * 'a"}), NoSyn)
-*}
-
-ML {* Sign.the_const_type @{theory} @{const_name c} *}
-
-declare [[ML_print_depth = 1000]]
-
-ML {*
-let
-  val (conjs, (defs, nondefs), _) = read_tptp_file @{theory} snd (* "/Users/blanchet/tmp/e.tptp" *)
-    "/Users/blanchet/.isabelle/prob_alt_ergo_1"
-  val ts = conjs @ defs @ nondefs
-    |> map (map_aterms (fn Const (s, T) =>
-        if String.isPrefix "TPTP" s then
-          Const (s |> Long_Name.base_name |> perhaps (try (unprefix "bnd_")), T)
-        else
-          Const (s, T)
-      | t => t))
-in
-  tracing (cat_lines (map (Syntax.string_of_term_global @{theory}) ts));
-  tracing (cat_lines (map @{make_string} ts))
-end
-*}
-
 end
\ No newline at end of file