author | haftmann |
Sat, 22 Sep 2012 21:59:40 +0200 | |
changeset 49533 | 484ac6cb13e6 |
parent 49532 | 6f7cc8e42716 |
child 49534 | 791e6fc53f73 |
--- 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 ()); );