# 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