1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Sep 02 16:20:09 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Sep 02 17:57:37 2011 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4           map (rpair (mk_type thy prfx ty)) flds) fldtys
     1.5         in case get_type thy prfx s of
     1.6             NONE =>
     1.7 -             Record.add_record true ([], Binding.name s) NONE
     1.8 +             Record.add_record ([], Binding.name s) NONE
     1.9                 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
    1.10           | SOME rT =>
    1.11               (case get_record_info thy rT of

     2.1 --- a/src/HOL/Tools/record.ML	Fri Sep 02 16:20:09 2011 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Fri Sep 02 17:57:37 2011 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    val get_info: theory -> string -> info option
     2.5    val the_info: theory -> string -> info
     2.6    val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
     2.7 -  val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
     2.8 +  val add_record: (string * sort) list * binding -> (typ list * string) option ->
     2.9      (binding * typ * mixfix) list -> theory -> theory
    2.10  
    2.11    val last_extT: typ -> (string * typ list) option
    2.12 @@ -2438,12 +2438,9 @@
    2.13  
    2.14  in
    2.15  
    2.16 -fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
    2.17 +fun add_record (params, binding) raw_parent raw_fields thy =
    2.18    let
    2.19      val _ = Theory.requires thy "Record" "record definitions";
    2.20 -    val _ =
    2.21 -      if quiet_mode then ()
    2.22 -      else writeln ("Defining record " ^ Binding.print binding ^ " ...");
    2.23  
    2.24      val ctxt = Proof_Context.init_global thy;
    2.25      fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
    2.26 @@ -2493,7 +2490,7 @@
    2.27    end
    2.28    handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
    2.29  
    2.30 -fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
    2.31 +fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
    2.32    let
    2.33      val ctxt = Proof_Context.init_global thy;
    2.34      val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
    2.35 @@ -2501,7 +2498,7 @@
    2.36      val (parent, ctxt2) = read_parent raw_parent ctxt1;
    2.37      val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
    2.38      val params' = map (Proof_Context.check_tfree ctxt3) params;
    2.39 -  in thy |> add_record quiet_mode (params', binding) parent fields end;
    2.40 +  in thy |> add_record (params', binding) parent fields end;
    2.41  
    2.42  end;
    2.43  
    2.44 @@ -2521,6 +2518,6 @@
    2.45      (Parse.type_args_constrained -- Parse.binding --
    2.46        (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
    2.47          Scan.repeat1 Parse.const_binding)
    2.48 -    >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
    2.49 +    >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
    2.50  
    2.51  end;