| changeset 25501 | 845883bd3a6b |
| parent 25485 | 33840a854e63 |
| child 25597 | 34860182b250 |
--- a/src/Pure/Isar/code.ML Wed Nov 28 19:54:50 2007 +0100 +++ b/src/Pure/Isar/code.ML Thu Nov 29 07:55:46 2007 +0100 @@ -383,7 +383,6 @@ val _ = Context.add_setup CodeData.init; -fun ch r f = let val x = f (! r) in (r := x; x) end; fun thy_data f thy = f ((snd o CodeData.get) thy); fun get_ensure_init kind data_ref =