prove_multi: immediate;
authorwenzelm
Tue, 23 Sep 2008 23:07:48 +0200
changeset 28341383f512314b9
parent 28340 e8597242f649
child 28342 d0db291f7194
prove_multi: immediate;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Tue Sep 23 22:04:30 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Sep 23 23:07:48 2008 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4      |> map Drule.zero_var_indexes
     1.5    end;
     1.6  
     1.7 -val prove_multi = prove_common false;
     1.8 +val prove_multi = prove_common true;
     1.9  
    1.10  fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
    1.11  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);