tuning

--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -17,12 +17,12 @@
 
   (*translation configuration*)
   type sign = {
-    header: string,
+    logic: string,
     sorts: string list,
     dtyps: (string * (string * (string * string) list) list) list list,
     funcs: (string * (string list * string)) list }
   type config = {
-    header: term list -> string,
+    logic: term list -> string,
     has_datatypes: bool,
     serialize: string list -> sign -> sterm list -> string }
   type replay_data = {
@@ -57,13 +57,13 @@
 (* translation configuration *)
 
 type sign = {
-  header: string,
+  logic: string,
   sorts: string list,
   dtyps: (string * (string * (string * string) list) list) list list,
   funcs: (string * (string list * string)) list }
 
 type config = {
-  header: term list -> string,
+  logic: term list -> string,
   has_datatypes: bool,
   serialize: string list -> sign -> sterm list -> string }
 
@@ -111,8 +111,8 @@
         val terms' = Termtab.update (t, (name, sort)) terms
       in (name, (names', typs, terms')) end)
 
-fun sign_of header dtyps (_, typs, terms) = {
-  header = header,
+fun sign_of logic dtyps (_, typs, terms) = {
+  logic = logic,
   sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
   dtyps = dtyps,
   funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
@@ -411,7 +411,7 @@
 
 (** translation from Isabelle terms into SMT intermediate terms **)
 
-fun intermediate header dtyps builtin ctxt ts trx =
+fun intermediate logic dtyps builtin ctxt ts trx =
   let
     fun transT (T as TFree _) = add_typ T true
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
@@ -448,7 +448,7 @@
       end
 
     val (us, trx') = fold_map trans ts trx
-  in ((sign_of (header ts) dtyps trx', us), trx') end
+  in ((sign_of (logic ts) dtyps trx', us), trx') end
 
 
 (* translation *)
@@ -474,7 +474,7 @@
 
 fun translate ctxt comments ithms =
   let
-    val {header, has_datatypes, serialize} = get_config ctxt
+    val {logic, has_datatypes, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
@@ -512,7 +512,7 @@
       |>> apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
-    |-> intermediate header dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
+    |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
     |>> uncurry (serialize comments)
     ||> replay_data_of ctxt2 rewrite_rules ithms
   end

--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -59,7 +59,7 @@
 
 (* serialization *)
 
-(** header **)
+(** logic **)
 
 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
 
@@ -128,11 +128,11 @@
 fun assert_name_of_index i = assert_prefix ^ string_of_int i
 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
 
-fun serialize comments {header, sorts, dtyps, funcs} ts =
+fun serialize comments {logic, sorts, dtyps, funcs} ts =
   Buffer.empty
   |> fold (Buffer.add o enclose "; " "\n") comments
   |> Buffer.add "(set-option :produce-proofs true)\n"
-  |> Buffer.add header
+  |> Buffer.add logic
   |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
   |> (if null dtyps then I
     else Buffer.add (enclose "(declare-datatypes () (" "))\n"
@@ -148,7 +148,7 @@
 (* interface *)
 
 fun translate_config ctxt = {
-  header = choose_logic ctxt,
+  logic = choose_logic ctxt,
   has_datatypes = false,
   serialize = serialize}
 

--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -31,7 +31,7 @@
 
 local
   fun translate_config ctxt =
-    {header = K "", has_datatypes = true,
+    {logic = K "", has_datatypes = true,
      serialize = #serialize (SMTLIB2_Interface.translate_config ctxt)}
 
   fun is_div_mod @{const div (int)} = true