--- a/src/Pure/Isar/proof.ML Thu Dec 18 21:10:39 2014 +0100
+++ b/src/Pure/Isar/proof.ML Fri Dec 19 12:36:50 2014 +0100
@@ -1100,8 +1100,7 @@
structure Result = Proof_Data
(
type T = thm option;
- val empty = NONE;
- fun init _ = empty;
+ fun init _ = NONE;
);
fun the_result ctxt =