1.1 --- a/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -8,8 +8,9 @@
     1.4  theory TPTP_Interpret
     1.5  imports Main TPTP_Parser
     1.6  keywords "import_tptp" :: thy_decl
     1.7 -uses
     1.8 -  "TPTP_Parser/tptp_interpret.ML"
     1.9 +uses  ("TPTP_Parser/tptp_interpret.ML")
    1.10  
    1.11  begin
    1.12 +typedecl "ind"
    1.13 +use  "TPTP_Parser/tptp_interpret.ML"
    1.14  end
    1.15 \ No newline at end of file

     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
     2.3 @@ -88,11 +88,6 @@
     2.4  
     2.5    (*Like "interpret_line" above, but works over a whole parsed problem.
     2.6      Arguments:
     2.7 -      new_basic_types = indicates whether interpretations of $i and $o
     2.8 -        types are to be added to the type map. This is "true" if we are
     2.9 -        running this over a fresh TPTP problem, but "false" if we are
    2.10 -        calling this _during_ the interpretation of a TPTP file
    2.11 -        (i.e. when interpreting an "include" directive).
    2.12        config = as previously
    2.13        inclusion list = as previously
    2.14        path_prefix = as previously
    2.15 @@ -101,7 +96,7 @@
    2.16        const_map = as previously
    2.17        thy = as previously
    2.18    *)
    2.19 -  val interpret_problem : bool -> config -> string list -> Path.T ->
    2.20 +  val interpret_problem : config -> string list -> Path.T ->
    2.21      TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory ->
    2.22      tptp_general_meaning * theory
    2.23  
    2.24 @@ -173,8 +168,6 @@
    2.25  fun type_exists thy ty_name =
    2.26    Sign.declared_tyname thy (Sign.full_bname thy ty_name)
    2.27  
    2.28 -val IND_TYPE = "ind"
    2.29 -
    2.30  (*transform quoted names into acceptable ASCII strings*)
    2.31  fun alphanumerate c =
    2.32    let
    2.33 @@ -280,7 +273,7 @@
    2.34           lookup_type type_map thf_ty
    2.35       | Defined_type tptp_base_type =>
    2.36           (case tptp_base_type of
    2.37 -            Type_Ind => lookup_type type_map thf_ty
    2.38 +            Type_Ind => @{typ ind}
    2.39            | Type_Bool => HOLogic.boolT
    2.40            | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
    2.41            | Type_Int => Type ("Int.int", [])
    2.42 @@ -689,7 +682,6 @@
    2.43    case line of
    2.44       Include (quoted_path, inc_list) =>
    2.45         interpret_file'
    2.46 -        false
    2.47          config
    2.48          inc_list
    2.49          path_prefix
    2.50 @@ -796,22 +788,9 @@
    2.51         else (*do nothing if we're not to includ this AF*)
    2.52           ((type_map, const_map, []), thy)
    2.53  
    2.54 -and interpret_problem new_basic_types config inc_list path_prefix lines
    2.55 - type_map const_map thy =
    2.56 +and interpret_problem config inc_list path_prefix lines type_map const_map thy =
    2.57    let
    2.58      val thy_name = Context.theory_name thy
    2.59 -    (*Add interpretation of $o and generate an Isabelle/HOL type to
    2.60 -    interpret $i, unless we've been given a mapping of types.*)
    2.61 -    val (thy', type_map') =
    2.62 -      if not new_basic_types then (thy, type_map)
    2.63 -      else
    2.64 -        let
    2.65 -          val (type_map', thy') =
    2.66 -            declare_type config
    2.67 -             (Defined_type Type_Ind, IND_TYPE) type_map thy
    2.68 -        in
    2.69 -          (thy', type_map')
    2.70 -        end
    2.71    in
    2.72      fold (fn line =>
    2.73             fn ((type_map, const_map, lines), thy) =>
    2.74 @@ -826,17 +805,17 @@
    2.75                  thy')
    2.76               end)
    2.77           lines (*lines of the problem file*)
    2.78 -         ((type_map', const_map, []), thy') (*initial values*)
    2.79 +         ((type_map, const_map, []), thy) (*initial values*)
    2.80    end
    2.81  
    2.82 -and interpret_file' new_basic_types config inc_list path_prefix file_name =
    2.83 +and interpret_file' config inc_list path_prefix file_name =
    2.84    let
    2.85      val file_name' = Path.expand file_name
    2.86    in
    2.87      if Path.is_absolute file_name' then
    2.88        Path.implode file_name
    2.89        |> TPTP_Parser.parse_file
    2.90 -      |> interpret_problem new_basic_types config inc_list path_prefix
    2.91 +      |> interpret_problem config inc_list path_prefix
    2.92      else error "Could not determine absolute path to file"
    2.93    end
    2.94  
    2.95 @@ -852,7 +831,7 @@
    2.96        {cautious = cautious,
    2.97         problem_name = NONE
    2.98        }
    2.99 -  in interpret_file' true config [] path_prefix file_name end
   2.100 +  in interpret_file' config [] path_prefix file_name end
   2.101  
   2.102  fun import_file cautious path_prefix file_name type_map const_map thy =
   2.103    let