src/HOL/Tools/record.ML

 
 (* parse translations *)
 
 local
 
-fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
-      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
-  | field_update_tr t = raise TERM ("field_update_tr", [t]);
-
-fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
-      field_update_tr t :: field_updates_tr u
-  | field_updates_tr t = [field_update_tr t];
-
-fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
-  | record_update_tr ts = raise TERM ("record_update_tr", ts);
+fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
+      (name, arg)
+  | field_type_tr t = raise TERM ("field_type_tr", [t]);
+
+fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
+      field_type_tr t :: field_types_tr u
+  | field_types_tr t = [field_type_tr t];
+
+fun record_field_types_tr more ctxt t =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
+
+    fun split_args (field :: fields) ((name, arg) :: fargs) =
+          if can (unsuffix name) field then
+            let val (args, rest) = split_args fields fargs
+            in (arg :: args, rest) end
+          else err ("expecting field " ^ field ^ " but got " ^ name)
+      | split_args [] (fargs as (_ :: _)) = ([], fargs)
+      | split_args (_ :: _) [] = err "expecting more fields"
+      | split_args _ _ = ([], []);
+
+    fun mk_ext (fargs as (name, _) :: _) =
+          (case get_fieldext thy (Sign.intern_const thy name) of
+            SOME (ext, alphas) =>
+              (case get_extfields thy ext of
+                SOME fields =>
+                  let
+                    val fields' = but_last fields;
+                    val types = map snd fields';
+                    val (args, rest) = split_args (map fst fields') fargs;
+                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
+                    val midx = fold Term.maxidx_typ argtypes 0;
+                    val varifyT = varifyT midx;
+                    val vartypes = map varifyT types;
+
+                    val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty
+                      handle Type.TYPE_MATCH => err "type is no proper record (extension)";
+                    val alphas' =
+                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
+                        (but_last alphas);
+
+                    val more' = mk_ext rest;
+                  in
+                    (* FIXME authentic syntax *)
+                    list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
+                  end
+              | NONE => err ("no fields defined for " ^ ext))
+          | NONE => err (name ^ " is no proper field"))
+      | mk_ext [] = more;
+  in
+    mk_ext (field_types_tr t)
+  end;
+
+(* FIXME @{type_syntax} *)
+fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t
+  | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
+
+fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
+  | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
 
 
 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
   | field_tr t = raise TERM ("field_tr", [t]);
 

 
 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
   | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
 
 
-fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
-      (name, arg)
-  | field_type_tr t = raise TERM ("field_type_tr", [t]);
-
-fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
-      field_type_tr t :: field_types_tr u
-  | field_types_tr t = [field_type_tr t];
-
-fun record_field_types_tr more ctxt t =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
-
-    fun split_args (field :: fields) ((name, arg) :: fargs) =
-          if can (unsuffix name) field then
-            let val (args, rest) = split_args fields fargs
-            in (arg :: args, rest) end
-          else err ("expecting field " ^ field ^ " but got " ^ name)
-      | split_args [] (fargs as (_ :: _)) = ([], fargs)
-      | split_args (_ :: _) [] = err "expecting more fields"
-      | split_args _ _ = ([], []);
-
-    fun mk_ext (fargs as (name, _) :: _) =
-          (case get_fieldext thy (Sign.intern_const thy name) of
-            SOME (ext, alphas) =>
-              (case get_extfields thy ext of
-                SOME fields =>
-                  let
-                    val fields' = but_last fields;
-                    val types = map snd fields';
-                    val (args, rest) = split_args (map fst fields') fargs;
-                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
-                    val midx = fold Term.maxidx_typ argtypes 0;
-                    val varifyT = varifyT midx;
-                    val vartypes = map varifyT types;
-
-                    val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty
-                      handle Type.TYPE_MATCH => err "type is no proper record (extension)";
-                    val alphas' =
-                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
-                        (but_last alphas);
-
-                    val more' = mk_ext rest;
-                  in
-                    (* FIXME authentic syntax *)
-                    list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
-                  end
-              | NONE => err ("no fields defined for " ^ ext))
-          | NONE => err (name ^ " is no proper field"))
-      | mk_ext [] = more;
-  in
-    mk_ext (field_types_tr t)
-  end;
-
-(* FIXME @{type_syntax} *)
-fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t
-  | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
-
-fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
-  | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
+fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
+      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
+  | field_update_tr t = raise TERM ("field_update_tr", [t]);
+
+fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
+      field_update_tr t :: field_updates_tr u
+  | field_updates_tr t = [field_update_tr t];
+
+fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
+  | record_update_tr ts = raise TERM ("record_update_tr", ts);
 
 in
 
 val parse_translation =
  [(@{syntax_const "_record_update"}, record_update_tr)];

 fun record_split_simproc P =
   Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
-          if quantifier = @{const_name All} orelse
-            quantifier = @{const_name all} orelse
+          if quantifier = @{const_name all} orelse
+            quantifier = @{const_name All} orelse
             quantifier = @{const_name Ex}
           then
             (case rec_id ~1 T of
               "" => NONE
             | _ =>

   end);
 
 
 (* record_split_tac *)
 
-(*Split all records in the goal, which are quantified by ALL or !!.*)
+(*Split all records in the goal, which are quantified by !! or ALL.*)
 val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   let
     val goal = term_of cgoal;
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
-          (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T
+          (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
         | _ => false);
 
     fun is_all t =
       (case t of
         Const (quantifier, _) $ _ =>
-          if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0
+          if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0
       | _ => 0);
   in
     if has_rec goal then
       Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
     else no_tac