src/Pure/Isar/locale.ML

     val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
     val err_msg =
       if forall (equal "" o #1) ids then msg
       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
-  in raise ProofContext.CONTEXT (err_msg, ctxt) end;
+  in error err_msg end;
 
 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
 
 
 

     val thy = ProofContext.theory_of ctxt;
 
     fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
       | renaming (NONE :: xs) (y :: ys) = renaming xs ys
       | renaming [] _ = []
-      | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
+      | renaming xs [] = error ("Too many arguments in renaming: " ^
           commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
 
     fun rename_parms top ren ((name, ps), (parms, mode)) =
       let val ps' = map (Element.rename ren) ps in
         (case duplicates ps' of

             in (ids_ax, merge_lists parms' ps, syn) end
       | identify top (Rename (e, xs)) =
           let
             val (ids', parms', syn') = identify top e;
             val ren = renaming xs parms'
-              handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
+              handle ERROR msg => err_in_locale' ctxt msg ids';
 
             val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
             val parms'' = distinct (List.concat (map (#2 o #1) ids''));
             val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make;
             (* check for conflicting syntax? *)

 fun activate_elems (((name, ps), mode), elems) ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val ((ctxt', _), res) =
         foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
-      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
+      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
     val ctxt'' = if name = "" then ctxt'
           else let
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
             in case mode of

 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
     let val (ctxt', propps) =
       (case elems of
         Int es => foldl_map declare_int_elem (ctxt, es)
       | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
-      handle ProofContext.CONTEXT (msg, ctxt) =>
-        err_in_locale ctxt msg [(name, map fst ps)]
+      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
     in (ctxt', propps) end
   | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
 
 in
 

           let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
             (Term.add_frees t []))
           in Term.list_all_free (frees, t) end;
 
         fun no_binds [] = []
-          | no_binds _ =
-              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
+          | no_binds _ = error "Illegal term bindings in locale element";
       in
         (case elem of
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>

 
 (* facts and attributes *)
 
 local
 
-fun prep_name ctxt name =
-  if NameSpace.is_qualified name then
-    raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
+fun prep_name name =
+  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   else name;
 
 fun prep_facts _ _ ctxt (Int elem) =
       Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
   | prep_facts get intern ctxt (Ext elem) = elem |> Element.map_ctxt
      {var = I, typ = I, term = I,
-      name = prep_name ctxt,
+      name = prep_name,
       fact = get ctxt,
       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
 
 in