1.1 --- a/Admin/update-keywords	Thu Mar 15 22:08:53 2012 +0100
     1.2 +++ b/Admin/update-keywords	Thu Mar 15 22:20:07 2012 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  isabelle keywords \
     1.5    "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
     1.6    "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
     1.7 -  "$LOG/HOL-SPARK.gz"
     1.8 +  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz"
     1.9  
    1.10  isabelle keywords -k ZF \
    1.11    "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

     2.1 --- a/etc/isar-keywords.el	Thu Mar 15 22:08:53 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Mar 15 22:20:07 2012 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK.
     2.7 +;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
    2.11 @@ -108,6 +108,7 @@
    2.12      "hide_const"
    2.13      "hide_fact"
    2.14      "hide_type"
    2.15 +    "import_tptp"
    2.16      "inductive"
    2.17      "inductive_cases"
    2.18      "inductive_set"
    2.19 @@ -484,6 +485,7 @@
    2.20      "hide_const"
    2.21      "hide_fact"
    2.22      "hide_type"
    2.23 +    "import_tptp"
    2.24      "inductive"
    2.25      "inductive_set"
    2.26      "instantiation"

     3.1 --- a/src/HOL/IsaMakefile	Thu Mar 15 22:08:53 2012 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Thu Mar 15 22:20:07 2012 +0100
     3.3 @@ -1232,14 +1232,21 @@
     3.4  
     3.5  HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz
     3.6  
     3.7 -$(LOG)/HOL-TPTP.gz: \
     3.8 -  $(OUT)/HOL \
     3.9 +$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \
    3.10 +  TPTP/ATP_Problem_Import.thy \
    3.11 +  TPTP/ATP_Theory_Export.thy \
    3.12 +  TPTP/CASC_Setup.thy \
    3.13    TPTP/ROOT.ML \
    3.14 +  TPTP/TPTP_Parser.thy \
    3.15 +  TPTP/TPTP_Parser/ml_yacc_lib.ML \
    3.16 +  TPTP/TPTP_Parser/tptp_interpret.ML \
    3.17 +  TPTP/TPTP_Parser/tptp_lexyacc.ML \
    3.18 +  TPTP/TPTP_Parser/tptp_parser.ML \
    3.19 +  TPTP/TPTP_Parser/tptp_problem_name.ML \
    3.20 +  TPTP/TPTP_Parser/tptp_syntax.ML \
    3.21 +  TPTP/TPTP_Parser_Test.thy \
    3.22    TPTP/atp_problem_import.ML \
    3.23 -  TPTP/ATP_Problem_Import.thy \
    3.24 -  TPTP/atp_theory_export.ML \
    3.25 -  TPTP/ATP_Theory_Export.thy \
    3.26 -  TPTP/CASC_Setup.thy
    3.27 +  TPTP/atp_theory_export.ML
    3.28  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
    3.29  
    3.30  

     4.1 --- a/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:08:53 2012 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:20:07 2012 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  theory TPTP_Parser
     4.6  imports Main
     4.7 -keywords "import_tptp" :: diag (* FIXME !? *) 
     4.8 +keywords "import_tptp" :: thy_decl 
     4.9  uses
    4.10    "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
    4.11  

     5.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Mar 15 22:08:53 2012 +0100
     5.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Mar 15 22:20:07 2012 +0100
     5.3 @@ -887,14 +887,9 @@
     5.4    in TPTP_Data.map (cons ((prob_name, result))) thy' end
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.improper_command "import_tptp" "import TPTP problem"
     5.8 -   Keyword.diag (*FIXME why diag?*)
     5.9 -   (Parse.string >>
    5.10 -    (fn file_name =>
    5.11 -      Toplevel.theory (fn thy =>
    5.12 -        import_file true (Path.explode file_name |> Path.dir)
    5.13 -         (Path.explode file_name) [] [] thy
    5.14 -        )))
    5.15 +  Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
    5.16 +    (Parse.path >> (fn path =>
    5.17 +      Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
    5.18  
    5.19  
    5.20  (*Used for debugging. Returns all files contained within a directory or its