author | haftmann |
Mon, 24 Sep 2012 19:11:35 +0200 | |
changeset 49556 | 47e4178f9a94 |
parent 49555 | fb2128470345 |
child 49557 | 61988f9df94d |
child 49576 | 6abbede3ae12 |
--- a/src/Pure/Isar/code.ML Mon Sep 24 17:52:44 2012 +0200 +++ b/src/Pure/Isar/code.ML Mon Sep 24 19:11:35 2012 +0200 @@ -283,7 +283,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 = apsnd (K (empty_dataref ())); + val extend : T -> T = apsnd (K (empty_dataref ())); fun merge ((spec1, _), (spec2, _)) = (merge_spec (spec1, spec2), empty_dataref ()); );