more uniform ordering and naming of sections;
proper local function

--- 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
@@ -191,9 +191,9 @@
 
 datatype spec = Spec of {
   history_concluded: bool,
-  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
+  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
     (*with explicit history*),
-  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
+  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
     (*with explicit history*),
   cases: ((int * (int * string option list)) * thm) Symtab.table,
   undefineds: unit Symtab.table
@@ -350,7 +350,7 @@
 
 (** foundation **)
 
-(* datatypes *)
+(* types *)
 
 fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
   ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
@@ -954,9 +954,11 @@
      |> cert_of_abs ctxt tyco c;
 
 
-(* cases *)
+(* case certificates *)
 
-fun case_certificate thm =
+local
+
+fun raw_case_cert thm =
   let
     val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
       o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
@@ -992,10 +994,14 @@
       | analyze cases = analyze_cases cases;
   in (case_const, (n, analyze cases)) end;
 
-fun case_cert thm = case_certificate thm
+in
+
+fun case_cert thm = raw_case_cert thm
   handle Bind => error "bad case certificate"
        | TERM _ => error "bad case certificate";
 
+end;
+
 fun get_case_scheme thy =
   Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
 fun get_case_cong thy =