changeset 17756 | d4a35f82fbb4 |
parent 17412 | e26cb20ef0cc |
child 18632 | 3149c6abe876 |
--- a/src/Pure/context.ML Tue Oct 04 16:47:40 2005 +0200 +++ b/src/Pure/context.ML Tue Oct 04 19:01:37 2005 +0200 @@ -314,7 +314,8 @@ fun create_thy name self id ids iids data ancestry history = let - val intermediate = #version history > 0; + val {version, name = _, intermediates = _} = history; + val intermediate = version > 0; val (ids', iids') = check_insert intermediate id (ids, iids); val id' = (serial (), name); val _ = check_insert intermediate id' (ids', iids');