src/HOL/TPTP/TPTP_Parser_Example.thy
changeset 47548 60849d8c457d
parent 47518 b2f209258621
child 47558 55b42f9af99d
     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 17:33:11 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 17:33:11 2012 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     1.5  begin
     1.6  
     1.7 -import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
     1.8 -(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
     1.9 +import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
    1.10  
    1.11  ML {*
    1.12  val an_fmlas =
    1.13 @@ -22,7 +21,7 @@
    1.14  
    1.15  (*Display nicely.*)
    1.16  ML {*
    1.17 -List.app (fn (n, role, _, fmla, _) =>
    1.18 +List.app (fn (n, role, fmla, _) =>
    1.19    Pretty.writeln
    1.20      (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
    1.21        TPTP_Syntax.role_to_string role  ^ "): "), Syntax.pretty_term @{context} fmla])
    1.22 @@ -35,9 +34,9 @@
    1.23  fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
    1.24   (string * term) list =
    1.25     let
    1.26 -     fun role_predicate (_, role, _, _, _) =
    1.27 +     fun role_predicate (_, role, _, _) =
    1.28         fold (fn r1 => fn b => role = r1 orelse b) roles false
    1.29 -   in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
    1.30 +   in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
    1.31  *}
    1.32  
    1.33  ML {*