tuned signature;
authorwenzelm
Thu Dec 15 22:22:45 2016 +0100 (2016-12-15)
changeset 64572cec07f7249cd
parent 64571 07bbdb2079db
child 64573 e6aee01da22d
tuned signature;
src/HOL/Proofs/ex/Proof_Terms.thy
src/Pure/Tools/thm_deps.ML
src/Pure/proofterm.ML
     1.1 --- a/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Dec 15 21:16:10 2016 +0100
     1.2 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Dec 15 22:22:45 2016 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4    (*all theorems used in the graph of nested proofs*)
     1.5    val all_thms =
     1.6      Proofterm.fold_body_thms
     1.7 -      (fn (name, _, _) => insert (op =) name) [body] [];
     1.8 +      (fn {name, ...} => insert (op =) name) [body] [];
     1.9  \<close>
    1.10  
    1.11  text \<open>
     2.1 --- a/src/Pure/Tools/thm_deps.ML	Thu Dec 15 21:16:10 2016 +0100
     2.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Dec 15 22:22:45 2016 +0100
     2.3 @@ -20,8 +20,8 @@
     2.4      fun make_node name directory =
     2.5        Graph_Display.session_node
     2.6         {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
     2.7 -    fun add_dep ("", _, _) = I
     2.8 -      | add_dep (name, _, PBody {thms = thms', ...}) =
     2.9 +    fun add_dep {name = "", ...} = I
    2.10 +      | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
    2.11            let
    2.12              val prefix = #1 (split_last (Long_Name.explode name));
    2.13              val session =
    2.14 @@ -73,7 +73,7 @@
    2.15  
    2.16      val used =
    2.17        Proofterm.fold_body_thms
    2.18 -        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    2.19 +        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
    2.20          (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
    2.21          Symtab.empty;
    2.22  
     3.1 --- a/src/Pure/proofterm.ML	Thu Dec 15 21:16:10 2016 +0100
     3.2 +++ b/src/Pure/proofterm.ML	Thu Dec 15 22:22:45 2016 +0100
     3.3 @@ -40,7 +40,8 @@
     3.4    val proof_of: proof_body -> proof
     3.5    val join_proof: proof_body future -> proof
     3.6    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     3.7 -  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
     3.8 +  val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     3.9 +    proof_body list -> 'a -> 'a
    3.10    val join_bodies: proof_body list -> unit
    3.11    val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    3.12  
    3.13 @@ -213,7 +214,7 @@
    3.14            let
    3.15              val body' = Future.join body;
    3.16              val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    3.17 -          in (f (name, prop, body') x', seen') end);
    3.18 +          in (f {serial = i, name = name, prop = prop, body = body'} x', seen') end);
    3.19    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    3.20  
    3.21  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();