author | lcp |

Thu Aug 18 17:53:28 1994 +0200 (1994-08-18) | |

changeset 545 | fc4ff96bb0e9 |

parent 544 | c53386a5bcf1 |

child 546 | 36e40454e03e |

Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved

from prove_goalw

from prove_goalw

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 [];