diff -r 2ee8333a2ba1 -r 08b06ec0ef74 src/Pure/Isar/proof.ML
--- 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