diff -r e903a1d0bed5 -r cbad888756b2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 03 00:06:23 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 03 00:06:24 2006 +0100
@@ -398,7 +398,12 @@
 val usingP =
   OuterSyntax.command "using" "augment goal facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+
+val unfoldingP =
+  OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
+    (K.tag_proof K.prf_decl)
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
 
 
 (* proof context *)
@@ -854,11 +859,12 @@
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
-  withP, noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
-  default_proofP, immediate_proofP, done_proofP, skip_proofP,
-  forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
-  finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
-  redoP, undos_proofP, undoP, killP, interpretationP, interpretP,
+  withP, noteP, usingP, unfoldingP, beginP, endP, nextP, qedP,
+  terminal_proofP, default_proofP, immediate_proofP, done_proofP,
+  skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
+  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
+  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
+  interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP,
   print_commandsP, print_contextP, print_theoryP, print_syntaxP,