# HG changeset patch
# User sultana
# Date 1334675647 -3600
# Node ID 9c3acd90063acbfaf6aca266fd4b89abe49921fc
# Parent  b2f209258621e762314ddc41bffe4abc61d1cb6a
simplified interpretation of '$i';

diff -r b2f209258621 -r 9c3acd90063a src/HOL/TPTP/TPTP_Interpret.thy
--- a/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -8,8 +8,9 @@
 theory TPTP_Interpret
 imports Main TPTP_Parser
 keywords "import_tptp" :: thy_decl
-uses
-  "TPTP_Parser/tptp_interpret.ML"
+uses  ("TPTP_Parser/tptp_interpret.ML")
 
 begin
+typedecl "ind"
+use  "TPTP_Parser/tptp_interpret.ML"
 end
\ No newline at end of file
diff -r b2f209258621 -r 9c3acd90063a src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
@@ -88,11 +88,6 @@
 
   (*Like "interpret_line" above, but works over a whole parsed problem.
     Arguments:
-      new_basic_types = indicates whether interpretations of $i and $o
-        types are to be added to the type map. This is "true" if we are
-        running this over a fresh TPTP problem, but "false" if we are
-        calling this _during_ the interpretation of a TPTP file
-        (i.e. when interpreting an "include" directive).
       config = as previously
       inclusion list = as previously
       path_prefix = as previously
@@ -101,7 +96,7 @@
       const_map = as previously
       thy = as previously
   *)
-  val interpret_problem : bool -> config -> string list -> Path.T ->
+  val interpret_problem : config -> string list -> Path.T ->
     TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory ->
     tptp_general_meaning * theory
 
@@ -173,8 +168,6 @@
 fun type_exists thy ty_name =
   Sign.declared_tyname thy (Sign.full_bname thy ty_name)
 
-val IND_TYPE = "ind"
-
 (*transform quoted names into acceptable ASCII strings*)
 fun alphanumerate c =
   let
@@ -280,7 +273,7 @@
          lookup_type type_map thf_ty
      | Defined_type tptp_base_type =>
          (case tptp_base_type of
-            Type_Ind => lookup_type type_map thf_ty
+            Type_Ind => @{typ ind}
           | Type_Bool => HOLogic.boolT
           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
           | Type_Int => Type ("Int.int", [])
@@ -689,7 +682,6 @@
   case line of
      Include (quoted_path, inc_list) =>
        interpret_file'
-        false
         config
         inc_list
         path_prefix
@@ -796,22 +788,9 @@
        else (*do nothing if we're not to includ this AF*)
          ((type_map, const_map, []), thy)
 
-and interpret_problem new_basic_types config inc_list path_prefix lines
- type_map const_map thy =
+and interpret_problem config inc_list path_prefix lines type_map const_map thy =
   let
     val thy_name = Context.theory_name thy
-    (*Add interpretation of $o and generate an Isabelle/HOL type to
-    interpret $i, unless we've been given a mapping of types.*)
-    val (thy', type_map') =
-      if not new_basic_types then (thy, type_map)
-      else
-        let
-          val (type_map', thy') =
-            declare_type config
-             (Defined_type Type_Ind, IND_TYPE) type_map thy
-        in
-          (thy', type_map')
-        end
   in
     fold (fn line =>
            fn ((type_map, const_map, lines), thy) =>
@@ -826,17 +805,17 @@
                 thy')
              end)
          lines (*lines of the problem file*)
-         ((type_map', const_map, []), thy') (*initial values*)
+         ((type_map, const_map, []), thy) (*initial values*)
   end
 
-and interpret_file' new_basic_types config inc_list path_prefix file_name =
+and interpret_file' config inc_list path_prefix file_name =
   let
     val file_name' = Path.expand file_name
   in
     if Path.is_absolute file_name' then
       Path.implode file_name
       |> TPTP_Parser.parse_file
-      |> interpret_problem new_basic_types config inc_list path_prefix
+      |> interpret_problem config inc_list path_prefix
     else error "Could not determine absolute path to file"
   end
 
@@ -852,7 +831,7 @@
       {cautious = cautious,
        problem_name = NONE
       }
-  in interpret_file' true config [] path_prefix file_name end
+  in interpret_file' config [] path_prefix file_name end
 
 fun import_file cautious path_prefix file_name type_map const_map thy =
   let