src/Pure/goal.ML

     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes
   end;
 
-val prove_multi = prove_common false;
+val prove_multi = prove_common true;
 
 fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =