src/HOL/Tools/record_package.ML

 
 val quiet_mode = ref false;
 fun message s = if ! quiet_mode then () else writeln s;
 
 
-(* fundamental syntax *)
+(* syntax *)
 
 fun prune n xs = Library.drop (n, xs);
-
 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);
 
 val Trueprop = HOLogic.mk_Trueprop;
 fun All xs t = Term.list_all_free (xs, t);
 

 val (op :==) = Logic.mk_defpair;
 val (op ===) = Trueprop o HOLogic.mk_eq;
 val (op ==>) = Logic.mk_implies;
 
 
-(* proof tools *)
+(* attributes *)
+
+val case_names_fields = RuleCases.case_names ["fields"];
+fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
+fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
+
+
+(* tactics *)
 
 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
 
 fun try_param_tac x s rule i st =
   res_inst_tac [(x, (case Tactic.innermost_params i st of [] => s | (p, _) :: _ => p))] rule i st;

 val sndN = "_more";
 val updateN = "_update";
 val makeN = "make";
 val extendN = "extend";
 val truncateN = "truncate";
-val fieldsN = "fields";
 
 
 (*see typedef_package.ML*)
 val RepN = "Rep_";
 val AbsN = "Abs_";

 fun add_parents thy None parents = parents
   | add_parents thy (Some (types, name)) parents =
       let
         val sign = Theory.sign_of thy;
         fun err msg = error (msg ^ " parent record " ^ quote name);
-    
+
         val {args, parent, fields, field_inducts, field_cases, simps} =
           (case get_record thy name of Some info => info | None => err "Unknown");
         val _ = if length types <> length args then err "Bad number of arguments for" else ();
-    
+
         fun bad_inst ((x, S), T) =
           if Sign.of_sort sign (T, S) then None else Some x
         val bads = mapfilter bad_inst (args ~~ types);
-    
+
         val inst = map fst args ~~ types;
         val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
         val parent' = apsome (apfst (map subst)) parent;
         val fields' = map (apsnd subst) fields;
       in
-        if not (null bads) then
-          err ("Ill-sorted instantiation of " ^ commas bads ^ " in")
-        else add_parents thy parent'
+        conditional (not (null bads)) (fn () =>
+          err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
+        add_parents thy parent'
           (make_parent_info name fields' field_inducts field_cases simps :: parents)
       end;
 
 
 

 val record_split_method =
   ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac),
     "split record fields");
 
 
+
 (** internal theory extenders **)
 
 (* field_typedefs *)
 
 fun field_typedefs zeta moreT names theory =

     val r_parent = if null parent_fields then [] else [Free (rN, hd parentT)];
 
     fun rec_schemeT n = mk_recordT (prune n all_fields, moreT);
     fun rec_scheme n = mk_record (prune n all_named_vars, more);
     fun recT n = mk_recordT (prune n all_fields, HOLogic.unitT);
-    fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit);    
+    fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit);
     fun r_scheme n = Free (rN, rec_schemeT n);
     fun r n = Free (rN, recT n);
 
 
     (* prepare print translation functions *)

     (*cases*)
     val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT));
     fun cases_scheme_prop n =
       All (prune n all_xs_more ~~ prune n all_types_more)
         ((r_scheme n === rec_scheme n) ==> C) ==> C;
-    fun cases_prop n =
-      All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
+    fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
 
 
     (* 1st stage: fields_thy *)
 
     val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =

 
     val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
       fields_thy
       |> add_record_splits named_splits
       |> Theory.parent_path
-      |> Theory.add_tyabbrs_i recordT_specs     (*not made part of record name space!*)
+      |> Theory.add_tyabbrs_i recordT_specs
       |> Theory.add_path bname
       |> Theory.add_trfuns ([], [], field_tr's, [])
       |> (Theory.add_consts_i o map Syntax.no_syn)
         (sel_decls @ update_decls @ [make_decl, extend_decl, truncate_decl])
       |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs

 
     val induct_scheme0 = induct_scheme 0;
     val cases_scheme0 = cases_scheme 0;
     val more_induct_scheme = map induct_scheme ancestry;
     val more_cases_scheme = map cases_scheme ancestry;
-
-    val case_names = RuleCases.case_names [fieldsN];
 
     val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _],
         [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
       defs_thy
       |> (PureThy.add_thmss o map Thm.no_attributes)

         ("update_convs", update_convs),
         ("select_defs", sel_defs),
         ("update_defs", update_defs),
         ("derived_defs", derived_defs)]
       |>>> PureThy.add_thms
-       [(("induct_scheme", induct_scheme0),
-         [case_names, InductAttrib.induct_type_global (suffix schemeN name)]),
-        (("cases_scheme", cases_scheme0),
-         [case_names, InductAttrib.cases_type_global (suffix schemeN name)])]
-      |>>> (PureThy.add_thmss o map Thm.no_attributes)
-        [("more_induct_scheme", more_induct_scheme),
-         ("more_cases_scheme", more_cases_scheme)];
+       [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
+        (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
+      |>>> PureThy.add_thmss
+        [(("more_induct_scheme", more_induct_scheme), induct_type_global ""),
+         (("more_cases_scheme", more_cases_scheme), cases_type_global "")];
 
 
     (* 4th stage: more_thms_thy *)
 
     val prove_standard = Tactic.prove_standard (Theory.sign_of thms_thy);

         THEN simp_all_tac HOL_basic_ss (parent_simps @ sel_convs))
       end);
 
     val (more_thms_thy, [_, _, equality']) =
       thms_thy |> PureThy.add_thms
-       [(("induct", induct0), [case_names, InductAttrib.induct_type_global name]),
-        (("cases", cases0), [case_names, InductAttrib.cases_type_global name]),
+       [(("induct", induct0), induct_type_global name),
+        (("cases", cases0), cases_type_global name),
         (("equality", equality), [Classical.xtra_intro_global])]
-      |>> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
-        [("more_induct", more_induct),
-         ("more_cases", more_cases)];
+      |>> (#1 oo PureThy.add_thmss)
+        [(("more_induct", more_induct), induct_type_global ""),
+         (("more_cases", more_cases), cases_type_global "")];
 
     val simps = sel_convs' @ update_convs' @ [equality'];
     val iffs = field_injects;
 
     val more_thms_thy' =