clarified context policy to allow multiple dummies;

--- 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