Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
authorlcp
Thu Aug 18 17:53:28 1994 +0200 (1994-08-18)
changeset 545fc4ff96bb0e9
parent 544 c53386a5bcf1
child 546 36e40454e03e
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
from prove_goalw
src/Pure/goals.ML
     1.1 --- a/src/Pure/goals.ML	Thu Aug 18 17:50:22 1994 +0200
     1.2 +++ b/src/Pure/goals.ML	Thu Aug 18 17:53:28 1994 +0200
     1.3 @@ -194,18 +194,19 @@
     1.4  	  (case Sequence.pull (tapply(tac,st0)) of 
     1.5  	       Some(st,_) => st
     1.6  	     | _ => error ("prove_goal: tactic failed"))
     1.7 -  in  mkresult (true, cond_timeit (!proof_timing) statef)  end;
     1.8 +  in  mkresult (true, cond_timeit (!proof_timing) statef)  end
     1.9 +  handle e => (print_sign_exn (#sign (rep_cterm chorn)) e;
    1.10 +	       error ("The exception above was raised for\n" ^ 
    1.11 +		      string_of_cterm chorn));
    1.12 +
    1.13  
    1.14  (*Version taking the goal as a string*)
    1.15  fun prove_goalw thy rths agoal tacsf =
    1.16    let val sign = sign_of thy
    1.17        val chorn = read_cterm sign (agoal,propT)
    1.18 -  in  prove_goalw_cterm rths chorn tacsf  
    1.19 -      handle ERROR => error (*from type_assign, etc via prepare_proof*)
    1.20 -		("The error above occurred for " ^ quote agoal)
    1.21 -       | e => (print_sign_exn sign e;	(*other exceptions*)
    1.22 -	       error ("The exception above was raised for " ^ quote agoal))
    1.23 -  end;
    1.24 +  in  prove_goalw_cterm rths chorn tacsf end
    1.25 +  handle ERROR => error (*from read_cterm?*)
    1.26 +		("The error above occurred for " ^ quote agoal);
    1.27  
    1.28  (*String version with no meta-rewrite-rules*)
    1.29  fun prove_goal thy = prove_goalw thy [];