removed conditional combinator;
authorwenzelm
Sat Dec 30 16:08:00 2006 +0100 (2006-12-30)
changeset 21962279b129498b6
parent 21961 8d34e64eeaf6
child 21963 416a5338d2bb
removed conditional combinator;
src/HOL/Tools/record_package.ML
src/HOL/ex/svc_funcs.ML
src/Pure/General/file.ML
src/Pure/General/name_space.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/toplevel.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/present.ML
src/Pure/Tools/codegen_data.ML
src/Pure/context.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Dec 30 12:41:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sat Dec 30 16:08:00 2006 +0100
     1.3 @@ -475,6 +475,7 @@
     1.4  
     1.5  val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
     1.6  
     1.7 +
     1.8  (* parent records *)
     1.9  
    1.10  fun add_parents thy NONE parents = parents
    1.11 @@ -490,6 +491,7 @@
    1.12          fun bad_inst ((x, S), T) =
    1.13            if Sign.of_sort sign (T, S) then NONE else SOME x
    1.14          val bads = List.mapPartial bad_inst (args ~~ types);
    1.15 +        val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
    1.16  
    1.17          val inst = map fst args ~~ types;
    1.18          val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    1.19 @@ -497,13 +499,12 @@
    1.20          val fields' = map (apsnd subst) fields;
    1.21          val extension' = apsnd (map subst) extension;
    1.22        in
    1.23 -        conditional (not (null bads)) (fn () =>
    1.24 -          err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
    1.25          add_parents thy parent'
    1.26 -          (make_parent_info name fields' extension' induct::parents)
    1.27 +          (make_parent_info name fields' extension' induct :: parents)
    1.28        end;
    1.29  
    1.30  
    1.31 +
    1.32  (** concrete syntax for records **)
    1.33  
    1.34  (* parse translations *)
     2.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Dec 30 12:41:59 2006 +0100
     2.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Dec 30 16:08:00 2006 +0100
     2.3 @@ -243,8 +243,7 @@
     2.4  
     2.5   (*The oracle proves the given formula t, if possible*)
     2.6   fun oracle thy t =
     2.7 -  (conditional (! trace) (fn () =>
     2.8 -    tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
     2.9 -  if valid (expr_of false t) then t else fail t);
    2.10 +  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else ();
    2.11 +   if valid (expr_of false t) then t else fail t);
    2.12  
    2.13  end;
     3.1 --- a/src/Pure/General/file.ML	Sat Dec 30 12:41:59 2006 +0100
     3.2 +++ b/src/Pure/General/file.ML	Sat Dec 30 16:08:00 2006 +0100
     3.3 @@ -137,12 +137,15 @@
     3.4      SOME ids => OS.FileSys.compare ids = EQUAL
     3.5    | NONE => false);
     3.6  
     3.7 -fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
     3.8 -  let val target = if is_dir dst then Path.append dst (Path.base src) else dst
     3.9 -  in write target (read src) end);
    3.10 +fun copy src dst =
    3.11 +  if eq (src, dst) then ()
    3.12 +  else
    3.13 +    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
    3.14 +    in write target (read src) end;
    3.15  
    3.16 -fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
    3.17 -  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
    3.18 +fun copy_dir src dst =
    3.19 +  if eq (src, dst) then ()
    3.20 +  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
    3.21  
    3.22  
    3.23  (* use ML files *)
     4.1 --- a/src/Pure/General/name_space.ML	Sat Dec 30 12:41:59 2006 +0100
     4.2 +++ b/src/Pure/General/name_space.ML	Sat Dec 30 16:08:00 2006 +0100
     4.3 @@ -232,11 +232,11 @@
     4.4    if is_hidden name then
     4.5      error ("Attempt to declare hidden name " ^ quote name)
     4.6    else
     4.7 -    let val names = explode_name name in
     4.8 -      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
     4.9 -        error ("Bad name declaration " ^ quote name));
    4.10 -      fold (add_name name) (map implode_name (accs names)) space
    4.11 -    end;
    4.12 +    let
    4.13 +      val names = explode_name name;
    4.14 +      val _ = (null names orelse exists (fn s => s = "") names) andalso
    4.15 +        error ("Bad name declaration " ^ quote name);
    4.16 +    in fold (add_name name) (map implode_name (accs names)) space end;
    4.17  
    4.18  
    4.19  (* manipulate namings *)
     5.1 --- a/src/Pure/Isar/locale.ML	Sat Dec 30 12:41:59 2006 +0100
     5.2 +++ b/src/Pure/Isar/locale.ML	Sat Dec 30 16:08:00 2006 +0100
     5.3 @@ -1070,10 +1070,10 @@
     5.4      val th = abstract_thm (ProofContext.theory_of ctxt) eq;
     5.5      fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
     5.6    in
     5.7 -    conditional (exists (equal y o #1) xs) (fn () =>
     5.8 -      err "Attempt to define previously specified variable");
     5.9 -    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
    5.10 -      err "Attempt to redefine variable");
    5.11 +    exists (equal y o #1) xs andalso
    5.12 +      err "Attempt to define previously specified variable";
    5.13 +    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
    5.14 +      err "Attempt to redefine variable";
    5.15      (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
    5.16    end;
    5.17  
    5.18 @@ -1763,8 +1763,8 @@
    5.19      do_predicate bname raw_import raw_body thy =
    5.20    let
    5.21      val name = Sign.full_name thy bname;
    5.22 -    val _ = conditional (is_some (get_locale thy name)) (fn () =>
    5.23 -      error ("Duplicate definition of locale " ^ quote name));
    5.24 +    val _ = is_some (get_locale thy name) andalso
    5.25 +      error ("Duplicate definition of locale " ^ quote name);
    5.26  
    5.27      val thy_ctxt = ProofContext.init thy;
    5.28      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
     6.1 --- a/src/Pure/Isar/method.ML	Sat Dec 30 12:41:59 2006 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Sat Dec 30 16:08:00 2006 +0100
     6.3 @@ -246,9 +246,10 @@
     6.4  val trace_rules = ref false;
     6.5  
     6.6  fun trace ctxt rules =
     6.7 -  conditional (! trace_rules andalso not (null rules)) (fn () =>
     6.8 +  if ! trace_rules andalso not (null rules) then
     6.9      Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
    6.10 -    |> Pretty.string_of |> tracing);
    6.11 +    |> Pretty.string_of |> tracing
    6.12 +  else ();
    6.13  
    6.14  local
    6.15  
     7.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 30 12:41:59 2006 +0100
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 30 16:08:00 2006 +0100
     7.3 @@ -661,8 +661,9 @@
     7.4  
     7.5  fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
     7.6    let
     7.7 -    val _ = conditional (not int andalso int_only) (fn () =>
     7.8 -      warning (command_msg "Interactive-only " tr));
     7.9 +    val _ =
    7.10 +      if not int andalso int_only then warning (command_msg "Interactive-only " tr)
    7.11 +      else ();
    7.12  
    7.13      fun do_timing f x = (Output.info (command_msg "" tr); timeap f x);
    7.14      fun do_profiling f x = profile (! profiling) f x;
    7.15 @@ -671,9 +672,9 @@
    7.16         state |> (apply_trans int trans
    7.17          |> (if ! profiling > 0 then do_profiling else I)
    7.18          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
    7.19 -    val _ = conditional (int andalso not (! quiet) andalso
    7.20 -        exists (member (op =) print) ("" :: ! print_mode))
    7.21 -      (fn () => print_state false result);
    7.22 +    val _ =
    7.23 +      if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)
    7.24 +      then print_state false result else ();
    7.25    in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
    7.26  
    7.27  in
     8.1 --- a/src/Pure/Syntax/ast.ML	Sat Dec 30 12:41:59 2006 +0100
     8.2 +++ b/src/Pure/Syntax/ast.ML	Sat Dec 30 16:08:00 2006 +0100
     8.3 @@ -205,8 +205,9 @@
     8.4        | rewrite ast = try_headless_rules ast;
     8.5  
     8.6      fun rewrote old_ast new_ast =
     8.7 -      conditional trace (fn () =>
     8.8 -        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast));
     8.9 +      if trace then
    8.10 +        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
    8.11 +      else ();
    8.12  
    8.13      fun norm_root ast =
    8.14        (case rewrite ast of
    8.15 @@ -234,17 +235,16 @@
    8.16        end;
    8.17  
    8.18  
    8.19 -    val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
    8.20 -
    8.21 +    val _ = if trace then tracing ("pre: " ^ str_of_ast pre_ast) else ();
    8.22      val post_ast = normal pre_ast;
    8.23 -  in
    8.24 -    conditional (trace orelse stat) (fn () =>
    8.25 -      tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
    8.26 -        string_of_int (! passes) ^ " passes, " ^
    8.27 -        string_of_int (! changes) ^ " changes, " ^
    8.28 -        string_of_int (! failed_matches) ^ " matches failed"));
    8.29 -    post_ast
    8.30 -  end;
    8.31 +    val _ =
    8.32 +      if trace orelse stat then
    8.33 +        tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
    8.34 +          string_of_int (! passes) ^ " passes, " ^
    8.35 +          string_of_int (! changes) ^ " changes, " ^
    8.36 +          string_of_int (! failed_matches) ^ " matches failed")
    8.37 +      else ();
    8.38 +  in post_ast end;
    8.39  
    8.40  
    8.41  (* normalize_ast *)
     9.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 30 12:41:59 2006 +0100
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 30 16:08:00 2006 +0100
     9.3 @@ -394,11 +394,12 @@
     9.4      fun show_pt pt =
     9.5        Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
     9.6    in
     9.7 -    conditional (length pts > ! ambiguity_level) (fn () =>
     9.8 +    if length pts > ! ambiguity_level then
     9.9        if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
    9.10        else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
    9.11            "produces " ^ string_of_int (length pts) ^ " parse trees.");
    9.12 -         List.app (warning o show_pt) pts));
    9.13 +         List.app (warning o show_pt) pts)
    9.14 +    else ();
    9.15      SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
    9.16    end;
    9.17  
    10.1 --- a/src/Pure/Thy/present.ML	Sat Dec 30 12:41:59 2006 +0100
    10.2 +++ b/src/Pure/Thy/present.ML	Sat Dec 30 16:08:00 2006 +0100
    10.3 @@ -305,8 +305,8 @@
    10.4  
    10.5        val (doc_prefix1, documents) =
    10.6          if doc = "" then (NONE, [])
    10.7 -        else if not (File.exists document_path) then (conditional verbose (fn () =>
    10.8 -          std_error "Warning: missing document directory\n"); (NONE, []))
    10.9 +        else if not (File.exists document_path) then
   10.10 +          (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, []))
   10.11          else (SOME (Path.append html_prefix document_path, html_prefix),
   10.12            read_versions doc_versions);
   10.13  
   10.14 @@ -341,10 +341,10 @@
   10.15        " 2>&1" ^ (if verbose then "" else " >/dev/null");
   10.16      val doc_path = Path.append result_path (Path.ext format (Path.basic name));
   10.17    in
   10.18 -    conditional verbose (fn () => writeln s);
   10.19 +    if verbose then writeln s else ();
   10.20      system s;
   10.21 -    conditional (not (File.exists doc_path)) (fn () =>
   10.22 -      error ("No document: " ^ quote (show_path doc_path)));
   10.23 +    File.exists doc_path orelse
   10.24 +      error ("No document: " ^ quote (show_path doc_path));
   10.25      doc_path
   10.26    end;
   10.27  
   10.28 @@ -399,7 +399,7 @@
   10.29        write_tex_index tex_index path;
   10.30        List.app (finish_tex path) thys);
   10.31    in
   10.32 -    conditional info (fn () =>
   10.33 +    if info then
   10.34       (File.mkdir (Path.append html_prefix session_path);
   10.35        Buffer.write (Path.append html_prefix pre_index_path) html_index;
   10.36        File.write (Path.append html_prefix session_entries_path) "";
   10.37 @@ -413,12 +413,12 @@
   10.38        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
   10.39        List.app finish_html thys;
   10.40        List.app (uncurry File.write) files;
   10.41 -      conditional verbose (fn () =>
   10.42 -        std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
   10.43 +      if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
   10.44 +    else ();
   10.45  
   10.46      (case doc_prefix2 of NONE => () | SOME (cp, path) =>
   10.47       (prepare_sources cp path;
   10.48 -      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
   10.49 +      if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
   10.50  
   10.51      (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
   10.52        documents |> List.app (fn (name, tags) =>
   10.53 @@ -426,7 +426,7 @@
   10.54           val _ = prepare_sources true path;
   10.55           val doc_path = isatool_document true doc_format name tags path result_path;
   10.56         in
   10.57 -         conditional verbose (fn () => std_error ("Document at " ^ show_path doc_path ^ "\n"))
   10.58 +         if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
   10.59         end));
   10.60  
   10.61      browser_info := empty_browser_info;
    11.1 --- a/src/Pure/Tools/codegen_data.ML	Sat Dec 30 12:41:59 2006 +0100
    11.2 +++ b/src/Pure/Tools/codegen_data.ML	Sat Dec 30 16:08:00 2006 +0100
    11.3 @@ -426,8 +426,10 @@
    11.4    let
    11.5      val k = serial ();
    11.6      val kind = {name = name, empty = empty, merge = merge, purge = purge};
    11.7 -    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    11.8 -      warning ("Duplicate declaration of code data " ^ quote name));
    11.9 +    val _ =
   11.10 +      if Datatab.exists (equal name o #name o #2) (! kinds) then
   11.11 +        warning ("Duplicate declaration of code data " ^ quote name)
   11.12 +      else ();
   11.13      val _ = change kinds (Datatab.update (k, kind));
   11.14    in k end;
   11.15  
    12.1 --- a/src/Pure/context.ML	Sat Dec 30 12:41:59 2006 +0100
    12.2 +++ b/src/Pure/context.ML	Sat Dec 30 16:08:00 2006 +0100
    12.3 @@ -145,8 +145,10 @@
    12.4    let
    12.5      val k = serial ();
    12.6      val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
    12.7 -    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    12.8 -      warning ("Duplicate declaration of theory data " ^ quote name));
    12.9 +    val _ =
   12.10 +      if Datatab.exists (equal name o #name o #2) (! kinds) then
   12.11 +        warning ("Duplicate declaration of theory data " ^ quote name)
   12.12 +      else ();
   12.13      val _ = change kinds (Datatab.update (k, kind));
   12.14    in k end;
   12.15  
   12.16 @@ -554,8 +556,10 @@
   12.17    let
   12.18      val k = serial ();
   12.19      val kind = {name = name, init = init};
   12.20 -    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   12.21 -      warning ("Duplicate declaration of proof data " ^ quote name));
   12.22 +    val _ =
   12.23 +      if Datatab.exists (equal name o #name o #2) (! kinds) then
   12.24 +        warning ("Duplicate declaration of proof data " ^ quote name)
   12.25 +      else ();
   12.26      val _ = change kinds (Datatab.update (k, kind));
   12.27    in k end;
   12.28  
    13.1 --- a/src/Pure/library.ML	Sat Dec 30 12:41:59 2006 +0100
    13.2 +++ b/src/Pure/library.ML	Sat Dec 30 16:08:00 2006 +0100
    13.3 @@ -75,7 +75,6 @@
    13.4    val toggle: bool ref -> bool
    13.5    val change: 'a ref -> ('a -> 'a) -> unit
    13.6    val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    13.7 -  val conditional: bool -> (unit -> unit) -> unit
    13.8  
    13.9    (*lists*)
   13.10    exception UnequalLengths
   13.11 @@ -395,11 +394,6 @@
   13.12    in release result end;
   13.13  
   13.14  
   13.15 -(* conditional execution *)
   13.16 -
   13.17 -fun conditional b f = if b then f () else ();
   13.18 -
   13.19 -
   13.20  
   13.21  (** lists **)
   13.22  
    14.1 --- a/src/Pure/meta_simplifier.ML	Sat Dec 30 12:41:59 2006 +0100
    14.2 +++ b/src/Pure/meta_simplifier.ML	Sat Dec 30 16:08:00 2006 +0100
    14.3 @@ -993,8 +993,10 @@
    14.4                   val b = Name.bound (#1 bounds);
    14.5                   val (v, t') = Thm.dest_abs (SOME b) t0;
    14.6                   val b' = #1 (Term.dest_Free (Thm.term_of v));
    14.7 -                 val _ = conditional (b <> b') (fn () =>
    14.8 -                   warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b'));
    14.9 +                 val _ =
   14.10 +                   if b <> b' then
   14.11 +                     warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
   14.12 +                   else ();
   14.13                   val ss' = add_bound ((b', T), a) ss;
   14.14                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
   14.15               in case botc skel' ss' t' of
   14.16 @@ -1171,18 +1173,20 @@
   14.17  
   14.18  val debug_bounds = ref false;
   14.19  
   14.20 -fun check_bounds ss ct = conditional (! debug_bounds) (fn () =>
   14.21 -  let
   14.22 -    val Simpset ({bounds = (_, bounds), ...}, _) = ss;
   14.23 -    val bs = fold_aterms (fn Free (x, _) =>
   14.24 -        if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
   14.25 -        then insert (op =) x else I
   14.26 -      | _ => I) (term_of ct) [];
   14.27 -  in
   14.28 -    if null bs then ()
   14.29 -    else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
   14.30 -      (Thm.theory_of_cterm ct) (Thm.term_of ct)
   14.31 -  end);
   14.32 +fun check_bounds ss ct =
   14.33 +  if ! debug_bounds then
   14.34 +    let
   14.35 +      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
   14.36 +      val bs = fold_aterms (fn Free (x, _) =>
   14.37 +          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
   14.38 +          then insert (op =) x else I
   14.39 +        | _ => I) (term_of ct) [];
   14.40 +    in
   14.41 +      if null bs then ()
   14.42 +      else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
   14.43 +        (Thm.theory_of_cterm ct) (Thm.term_of ct)
   14.44 +    end
   14.45 +  else ();
   14.46  
   14.47  fun rewrite_cterm mode prover raw_ss raw_ct =
   14.48    let
   14.49 @@ -1190,8 +1194,10 @@
   14.50      val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
   14.51      val ss = fallback_context thy raw_ss;
   14.52      val _ = inc simp_depth;
   14.53 -    val _ = conditional (!simp_depth mod 20 = 0) (fn () =>
   14.54 -      warning ("Simplification depth " ^ string_of_int (! simp_depth)));
   14.55 +    val _ =
   14.56 +      if ! simp_depth mod 20 = 0 then
   14.57 +        warning ("Simplification depth " ^ string_of_int (! simp_depth))
   14.58 +      else ();
   14.59      val _ = trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct;
   14.60      val _ = check_bounds ss ct;
   14.61      val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct
    15.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Dec 30 12:41:59 2006 +0100
    15.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Dec 30 16:08:00 2006 +0100
    15.3 @@ -148,8 +148,10 @@
    15.4    val big_rec_name = Sign.intern_const thy big_rec_base_name;
    15.5  
    15.6  
    15.7 -  val dummy = conditional verbose (fn () =>
    15.8 -    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
    15.9 +  val _ =
   15.10 +    if verbose then
   15.11 +      writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)
   15.12 +    else ();
   15.13  
   15.14    (*Forbid the inductive definition structure from clashing with a theory
   15.15      name.  This restriction may become obsolete as ML is de-emphasized.*)