changeset 67405 | e9ab4ad7bd15 |
parent 67399 | eab6ce8368fa |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Thu Jan 11 12:32:07 2018 +0100 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Thu Jan 11 13:48:17 2018 +0100 @@ -35,7 +35,7 @@ (*all theorems used in the graph of nested proofs*) val all_thms = Proofterm.fold_body_thms - (fn {name, ...} => insert (=) name) [body] []; + (fn {name, ...} => insert (op =) name) [body] []; \<close> text \<open>