# HG changeset patch
# User wenzelm
# Date 1138727974 -3600
# Node ID 08b06ec0ef74597122b178cb0284916dbb5666ec
# Parent  2ee8333a2ba152979beb8d494a1326f8bda2887f
tuned LocalDefs.unfold;

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