1.1 --- a/src/HOL/Tools/meson.ML	Wed Oct 18 10:07:36 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Oct 18 10:15:39 2006 +0200
     1.3 @@ -91,12 +91,22 @@
     1.4          | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
     1.5    in  tryall rls  end;
     1.6    
     1.7 -(*Permits forward proof from rules that discharge assumptions*)
     1.8 +(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
     1.9 +  e.g. from conj_forward, should have the form
    1.10 +    "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
    1.11 +  and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    1.12  fun forward_res nf st =
    1.13 -  case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
    1.14 -  of SOME(th,_) => th
    1.15 -   | NONE => raise THM("forward_res", 0, [st]);
    1.16 -
    1.17 +  let fun forward_tacf [prem] = rtac (nf prem) 1
    1.18 +        | forward_tacf prems = 
    1.19 +            error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
    1.20 +                   string_of_thm st ^
    1.21 +                   "\nPremises:\n" ^
    1.22 +                   cat_lines (map string_of_thm prems))
    1.23 +  in
    1.24 +    case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
    1.25 +    of SOME(th,_) => th
    1.26 +     | NONE => raise THM("forward_res", 0, [st])
    1.27 +  end;
    1.28  
    1.29  (*Are any of the logical connectives in "bs" present in the term?*)
    1.30  fun has_conns bs =
    1.31 @@ -421,9 +431,11 @@
    1.32      HOL_basic_ss addsimps nnf_extra_simps 
    1.33                   addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.34  
    1.35 -fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.36 -                     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    1.37 -                     |> make_nnf1
    1.38 +fun make_nnf th = case prems_of th of
    1.39 +    [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.40 +	     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    1.41 +	     |> make_nnf1
    1.42 +  | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.43  
    1.44  (*Pull existential quantifiers to front. This accomplishes Skolemization for
    1.45    clauses that arise from a subgoal.*)