--- a/src/Pure/Isar/proof.ML Tue Jan 31 18:19:32 2006 +0100
+++ b/src/Pure/Isar/proof.ML Tue Jan 31 18:19:34 2006 +0100
@@ -640,8 +640,8 @@
in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
fun append_using _ ths using = using @ ths;
-fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt true ths);
-fun unfold_goals ctxt ths = LocalDefs.unfold_goals ctxt true ths;
+fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
+val unfold_goals = LocalDefs.unfold_goals;
in