# HG changeset patch
# User wenzelm
# Date 1450898624 -3600
# Node ID a10cc7fb184140fa1f9eb2ee2058d6d7ef1fd2d6
# Parent  a1b697a2f3a8b9dd2db5ede1ddc5a9825f064875
clarified context policy to allow multiple dummies;

diff -r a1b697a2f3a8 -r a10cc7fb1841 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Dec 23 17:35:07 2015 +0100
+++ b/src/Pure/variable.ML	Wed Dec 23 20:23:44 2015 +0100
@@ -475,7 +475,7 @@
 (* dummy patterns *)
 
 fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt =
-      let val ([x], ctxt') = add_fixes [Name.uu_] ctxt
+      let val ([x], ctxt') = ctxt |> set_body true |> add_fixes [Name.uu_] ||> restore_body ctxt
       in (Free (x, T), ctxt') end
   | fix_dummy_patterns (Abs (x, T, b)) ctxt =
       let val (b', ctxt') = fix_dummy_patterns b ctxt