changeset 49556 | 47e4178f9a94 |
parent 49535 | e016736fbe0a |
child 49760 | 0721b1311327 |
--- 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 ()); );