# HG changeset patch
# User haftmann
# Date 1497938516 -7200
# Node ID 8a3b141179c25b12c97da6c70488309d2a78db1c
# Parent  0181bb24bdcadb15b9cc5bc421bd5c453f029730
avoid name particle "the" where no selection is implied

diff -r 0181bb24bdca -r 8a3b141179c2 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
@@ -232,10 +232,10 @@
   in make_spec (false, (functions, (types, (cases, undefineds)))) end;
 
 fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
-fun the_functions (Spec { functions, ... }) = functions;
-fun the_types (Spec { types, ... }) = types;
-fun the_cases (Spec { cases, ... }) = cases;
-fun the_undefineds (Spec { undefineds, ... }) = undefineds;
+fun types_of (Spec { types, ... }) = types;
+fun functions_of (Spec { functions, ... }) = functions;
+fun cases_of (Spec { cases, ... }) = cases;
+fun undefineds_of (Spec { undefineds, ... }) = undefineds;
 val map_history_concluded = map_spec o apfst;
 val map_functions = map_spec o apsnd o apfst;
 val map_typs = map_spec o apsnd o apsnd o apfst;
@@ -295,7 +295,7 @@
 
 (* access to executable code *)
 
-val the_exec : theory -> spec = fst o Code_Data.get;
+val spec_of : theory -> spec = fst o Code_Data.get;
 
 fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
 
@@ -306,13 +306,13 @@
 
 (* tackling equation history *)
 
-fun continue_history thy = if (history_concluded o the_exec) thy
+fun continue_history thy = if (history_concluded o spec_of) thy
   then thy
     |> (Code_Data.map o apfst o map_history_concluded) (K false)
     |> SOME
   else NONE;
 
-fun conclude_history thy = if (history_concluded o the_exec) thy
+fun conclude_history thy = if (history_concluded o spec_of) thy
   then NONE
   else thy
     |> (Code_Data.map o apfst)
@@ -395,7 +395,7 @@
     val constructors = map (inst vs o snd) raw_constructors;
   in (tyco, (map (rpair []) vs, constructors)) end;
 
-fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+fun get_type_entry thy tyco = case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
 
@@ -909,7 +909,7 @@
 (* code certificate access with preprocessing *)
 
 fun retrieve_raw thy c =
-  Symtab.lookup ((the_functions o the_exec) thy) c
+  Symtab.lookup ((functions_of o spec_of) thy) c
   |> Option.map (snd o fst)
   |> the_default Unimplemented
 
@@ -1003,11 +1003,11 @@
 end;
 
 fun get_case_scheme thy =
-  Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
+  Option.map fst o (Symtab.lookup o cases_of o spec_of) thy;
 fun get_case_cong thy =
-  Option.map snd o (Symtab.lookup o the_cases o the_exec) thy;
+  Option.map snd o (Symtab.lookup o cases_of o spec_of) thy;
 
-val undefineds = Symtab.keys o the_undefineds o the_exec;
+val undefineds = Symtab.keys o undefineds_of o spec_of;
 
 
 (* diagnostic *)
@@ -1015,7 +1015,7 @@
 fun print_codesetup thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val exec = the_exec thy;
+    val exec = spec_of thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks)
         (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
@@ -1047,17 +1047,17 @@
       | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
           Pretty.str (string_of_const thy const), Pretty.str "with",
           (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
-    val functions = the_functions exec
+    val functions = functions_of exec
       |> Symtab.dest
       |> (map o apsnd) (snd o fst)
       |> sort (string_ord o apply2 fst);
-    val datatypes = the_types exec
+    val datatypes = types_of exec
       |> Symtab.dest
       |> map (fn (tyco, (_, (vs, spec)) :: _) =>
           ((tyco, vs), constructors_of spec))
       |> sort (string_ord o apply2 (fst o fst));
-    val cases = Symtab.dest ((the_cases o the_exec) thy);
-    val undefineds = Symtab.keys ((the_undefineds o the_exec) thy);
+    val cases = Symtab.dest ((cases_of o spec_of) thy);
+    val undefineds = Symtab.keys ((undefineds_of o spec_of) thy);
   in
     Pretty.writeln_chunks [
       Pretty.block (
@@ -1253,7 +1253,7 @@
 fun register_type (tyco, vs_spec) thy =
   let
     val (old_constrs, some_old_proj) =
-      case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+      case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
        of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
         | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
         | [] => ([], NONE);
@@ -1264,7 +1264,7 @@
           (fn (c, ((_, spec), _)) =>
             if member (op =) (the_list (associated_abstype spec)) tyco
             then insert (op =) c else I)
-            ((the_functions o the_exec) thy) [old_proj];
+            ((functions_of o spec_of) thy) [old_proj];
     fun drop_outdated_cases cases = fold Symtab.delete_safe
       (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
         if exists (member (op =) old_constrs) (map_filter I cos)