changeset 12123 | 739eba13e2cd |
parent 11911 | 6533ceee4cd7 |
child 12151 | fb0fb0209c87 |
--- a/src/Pure/Thy/present.ML Fri Nov 09 00:18:23 2001 +0100 +++ b/src/Pure/Thy/present.ML Fri Nov 09 00:19:20 2001 +0100 @@ -78,6 +78,7 @@ val empty = {name = "Pure", session = [], is_local = false}; val copy = I; + val finish = I; fun prep_ext _ = {name = "", session = [], is_local = false}; fun merge _ = empty; fun print _ _ = ();