src/Pure/context.ML
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');