removed comments -- no exception TERM;
authorwenzelm
Thu Jul 05 20:01:37 2007 +0200 (2007-07-05)
changeset 236005a5332e1351b
parent 23599 d889725b0d8a
child 23601 3a40294140f0
removed comments -- no exception TERM;
merge_list: exception THEORY;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Jul 05 20:01:36 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Jul 05 20:01:37 2007 +0200
     1.3 @@ -34,9 +34,9 @@
     1.4    val defs_of : theory -> Defs.T
     1.5    val self_ref: theory -> theory_ref
     1.6    val deref: theory_ref -> theory
     1.7 -  val merge: theory * theory -> theory                     (*exception TERM*)
     1.8 -  val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
     1.9 -  val merge_list: theory list -> theory                    (*exception TERM*)
    1.10 +  val merge: theory * theory -> theory
    1.11 +  val merge_refs: theory_ref * theory_ref -> theory_ref
    1.12 +  val merge_list: theory list -> theory
    1.13    val requires: theory -> string -> string -> unit
    1.14    val assert_super: theory -> theory -> theory
    1.15    val cert_axm: theory -> string * term -> string * term
    1.16 @@ -70,7 +70,7 @@
    1.17  val merge = Context.merge;
    1.18  val merge_refs = Context.merge_refs;
    1.19  
    1.20 -fun merge_list [] = raise TERM ("Empty merge of theories", [])
    1.21 +fun merge_list [] = raise THEORY ("Empty merge of theories", [])
    1.22    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
    1.23  
    1.24  val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;