changeset 64572 | cec07f7249cd |
parent 62922 | 96691631c1eb |
child 64986 | b81a048960a3 |
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Thu Dec 15 21:16:10 2016 +0100 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Thu Dec 15 22:22:45 2016 +0100 @@ -30,7 +30,7 @@ (*all theorems used in the graph of nested proofs*) val all_thms = Proofterm.fold_body_thms - (fn (name, _, _) => insert (op =) name) [body] []; + (fn {name, ...} => insert (op =) name) [body] []; \<close> text \<open>