| changeset 47245 | ff1770df59b8 |
| parent 47240 | 72ab1fbf2f41 |
| child 47246 | 2bbab021c0e6 |
--- a/src/Pure/Isar/generic_target.ML Sun Apr 01 09:12:03 2012 +0200 +++ b/src/Pure/Isar/generic_target.ML Sun Apr 01 14:29:22 2012 +0200 @@ -191,7 +191,7 @@ fun standard_declaration decl = background_declaration decl #> - (fn lthy => Local_Theory.map_contexts (fn ctxt => + (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt => Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);