# HG changeset patch
# User blanchet
# Date 1407246887 -7200
# Node ID 07521fed607134eab8ef6f71a9a0d0bbbc543aec
# Parent  385d49c83943fc5187234d752d45ff9f954631ea
correctly interpret arithmetic types

diff -r 385d49c83943 -r 07521fed6071 src/HOL/TPTP/TPTP_Interpret.thy
--- a/src/HOL/TPTP/TPTP_Interpret.thy	Tue Aug 05 14:02:47 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Aug 05 15:54:47 2014 +0200
@@ -6,12 +6,12 @@
 *)
 
 theory TPTP_Interpret
-imports Main TPTP_Parser
+imports Complex_Main TPTP_Parser
 keywords "import_tptp" :: thy_decl
 begin
 
-typedecl "ind"
+typedecl ind
 
-ML_file  "TPTP_Parser/tptp_interpret.ML"
+ML_file "TPTP_Parser/tptp_interpret.ML"
 
 end
\ No newline at end of file
diff -r 385d49c83943 -r 07521fed6071 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Aug 05 14:02:47 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Aug 05 15:54:47 2014 +0200
@@ -270,15 +270,9 @@
             Type_Ind => @{typ ind}
           | Type_Bool => HOLogic.boolT
           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
-         (*FIXME these types are currently unsupported, so they're treated as
-         individuals*)
-          | Type_Int =>
-              interpret_type config thy type_map (Defined_type Type_Ind)
-          | Type_Rat =>
-              interpret_type config thy type_map (Defined_type Type_Ind)
-          | Type_Real =>
-              interpret_type config thy type_map (Defined_type Type_Ind)
-          )
+          | Type_Int => @{typ int}
+          | Type_Rat => @{typ rat}
+          | Type_Real => @{typ real})
      | Sum_type _ =>
          raise MISINTERPRET_TYPE (*FIXME*)
           ("No type interpretation (sum type)", thf_ty)