# HG changeset patch
# User wenzelm
# Date 1183658492 -7200
# Node ID 7ca68a2c85751cb3870a0112f1a90219bb75beb0
# Parent  e65e466dda01f98c70f77a30bbcfbadbb23e726e
the_theory/proof: error instead of exception Fail;

diff -r e65e466dda01 -r 7ca68a2c8575 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Jul 05 20:01:31 2007 +0200
+++ b/src/Pure/context.ML	Thu Jul 05 20:01:32 2007 +0200
@@ -475,8 +475,8 @@
 fun mapping f g = cases (Theory o f) (Proof o g);
 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
 
-val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected");
-val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I;
+val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
+val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
 
 fun map_theory f = Theory o f o the_theory;
 fun map_proof f = Proof o f o the_proof;