src/Pure/context.ML

 
 (* primitives *)
 
 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');
     val identity' = make_identity self id' ids' iids';
   in vitalize (Theory (identity', data, ancestry, history)) end;