src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59858 890b68e1e8b6
parent 59780 23b67731f4f0
child 59882 ada832308efe
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 30 20:51:11 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 30 22:34:59 2015 +0200
     1.3 @@ -2057,9 +2057,9 @@
     1.4            fun values () =
     1.5              case role of
     1.6                  TPTP_Syntax.Role_Definition =>
     1.7 -                  map (apsnd Binding.dest) (#defs pannot)
     1.8 +                  map (apsnd Binding.name_of) (#defs pannot)
     1.9                | TPTP_Syntax.Role_Axiom =>
    1.10 -                  map (apsnd Binding.dest) (#axs pannot)
    1.11 +                  map (apsnd Binding.name_of) (#axs pannot)
    1.12                | _ => raise UNSUPPORTED_ROLE
    1.13            in
    1.14              if is_none (source_inf_opt node) then []
    1.15 @@ -2075,7 +2075,7 @@
    1.16                           use the ones in the proof annotation.*)
    1.17                         (fn x =>
    1.18                           if role = TPTP_Syntax.Role_Definition then
    1.19 -                           let fun values () = map (apsnd Binding.dest) (#defs pannot)
    1.20 +                           let fun values () = map (apsnd Binding.name_of) (#defs pannot)
    1.21                             in
    1.22                               map snd (values ())
    1.23                             end
    1.24 @@ -2086,7 +2086,7 @@
    1.25  
    1.26        val roled_dependencies =
    1.27          roled_dependencies_names
    1.28 -        #> map (#3 #> Global_Theory.get_thm thy)
    1.29 +        #> map (Global_Theory.get_thm thy)
    1.30      in
    1.31        val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
    1.32        val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom