cache should not contain material from descendant theory
authorhaftmann
Sat, 22 Sep 2012 21:59:40 +0200
changeset 49533 484ac6cb13e6
parent 49532 6f7cc8e42716
child 49534 791e6fc53f73
cache should not contain material from descendant theory
src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Sep 22 21:23:16 2012 +0200
+++ b/src/Pure/Isar/code.ML	Sat Sep 22 21:59:40 2012 +0200
@@ -266,7 +266,7 @@
   type T = spec * (data * theory_ref) option Synchronized.var;
   val empty = (make_spec (false, (Symtab.empty,
     (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
-  val extend = I  (* FIXME empty_dataref!?! *)
+  val extend = apsnd (K (empty_dataref ()));
   fun merge ((spec1, _), (spec2, _)) =
     (merge_spec (spec1, spec2), empty_dataref ());
 );