# HG changeset patch
# User wenzelm
# Date 1183658497 -7200
# Node ID 5a5332e1351b23c2fef342655f8f2238640ccf2d
# Parent  d889725b0d8aff8f8b9bb966f839de50bb698da4
removed comments -- no exception TERM;
merge_list: exception THEORY;

diff -r d889725b0d8a -r 5a5332e1351b src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 05 20:01:36 2007 +0200
+++ b/src/Pure/theory.ML	Thu Jul 05 20:01:37 2007 +0200
@@ -34,9 +34,9 @@
   val defs_of : theory -> Defs.T
   val self_ref: theory -> theory_ref
   val deref: theory_ref -> theory
-  val merge: theory * theory -> theory                     (*exception TERM*)
-  val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
-  val merge_list: theory list -> theory                    (*exception TERM*)
+  val merge: theory * theory -> theory
+  val merge_refs: theory_ref * theory_ref -> theory_ref
+  val merge_list: theory list -> theory
   val requires: theory -> string -> string -> unit
   val assert_super: theory -> theory -> theory
   val cert_axm: theory -> string * term -> string * term
@@ -70,7 +70,7 @@
 val merge = Context.merge;
 val merge_refs = Context.merge_refs;
 
-fun merge_list [] = raise TERM ("Empty merge of theories", [])
+fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
 
 val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;