| changeset 36545 | 5c5b5c7f1157 |
| parent 36543 | 0e7fc5bf38de |
| child 36600 | 62d43ca574d0 |
--- a/src/Pure/simplifier.ML Thu Apr 29 23:55:43 2010 +0200 +++ b/src/Pure/simplifier.ML Fri Apr 30 17:18:29 2010 +0200 @@ -108,7 +108,7 @@ ); val get_ss = SimpsetData.get; -val map_ss = SimpsetData.map; +fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context; (* attributes *)