changeset 16850 | 35e07087aba2 |
parent 16790 | be2780f435e1 |
child 16861 | 7446b4be013b |
--- a/src/Pure/Isar/proof_context.ML Thu Jul 14 19:28:33 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Jul 14 19:28:34 2005 +0200 @@ -723,7 +723,7 @@ fn th => (case Seq.pull (exp th) of SOME (th', _) => th' |> Drule.local_standard - | NONE => raise CONTEXT ("Internal failure while exporting theorem", inner)) + | NONE => sys_error "Failed to export theorem") end; val export_standard = gen_export_std export_view;