# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 34bd10a9a2adca417e16f47762f3d76d6ef831ad
# Parent  99c82a837f8ad56abef403eddc74750b7e816df0
adapted to renamed ML files

diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/SMT2.thy	Thu Mar 13 13:18:14 2014 +0100
@@ -9,7 +9,7 @@
 keywords "smt2_status" :: diag
 begin
 
-ML_file "Tools/SMT2/smt2_utils.ML"
+ML_file "Tools/SMT2/smt2_util.ML"
 ML_file "Tools/SMT2/smt2_failure.ML"
 ML_file "Tools/SMT2/smt2_config.ML"
 
@@ -51,7 +51,7 @@
 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
 
 text {*
-Weights must be non-negative.  The value @{text 0} is equivalent to providing
+Weights must be nonnegative.  The value @{text 0} is equivalent to providing
 no weight at all.
 
 Weights should only be used at quantifiers and only inside triggers (if the
@@ -105,14 +105,14 @@
 ML_file "Tools/SMT2/z3_new_model.ML"
 ML_file "Tools/SMT2/z3_new_proof.ML"
 ML_file "Tools/SMT2/smt2_solver.ML"
+ML_file "Tools/SMT2/z3_new_isar.ML"
 ML_file "Tools/SMT2/z3_new_interface.ML"
-ML_file "Tools/SMT2/z3_new_proof_tools.ML"
-ML_file "Tools/SMT2/z3_new_proof_literals.ML"
-ML_file "Tools/SMT2/z3_new_proof_rules.ML"
-ML_file "Tools/SMT2/z3_new_proof_methods.ML"
-ML_file "Tools/SMT2/z3_new_proof_replay.ML"
-ML_file "Tools/SMT2/z3_new_isar.ML"
-ML_file "Tools/SMT2/smt2_setup_solvers.ML"
+ML_file "Tools/SMT2/z3_new_replay_util.ML"
+ML_file "Tools/SMT2/z3_new_replay_literals.ML"
+ML_file "Tools/SMT2/z3_new_replay_rules.ML"
+ML_file "Tools/SMT2/z3_new_replay_methods.ML"
+ML_file "Tools/SMT2/z3_new_replay.ML"
+ML_file "Tools/SMT2/smt2_systems.ML"
 
 method_setup smt2 = {*
   Scan.optional Attrib.thms [] >>
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_builtin.ML
--- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -10,9 +10,9 @@
   val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
 
   (*built-in types*)
-  val add_builtin_typ: SMT2_Utils.class ->
-    typ * (typ -> string option) * (typ -> int -> string option) ->
-    Context.generic -> Context.generic
+  val add_builtin_typ: SMT2_Util.class ->
+    typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+    Context.generic
   val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
     Context.generic
   val dest_builtin_typ: Proof.context -> typ -> string option
@@ -26,10 +26,9 @@
   (*built-in functions*)
   type 'a bfun = Proof.context -> typ -> term list -> 'a
   type bfunr = string * int * term list * (term list -> term)
-  val add_builtin_fun: SMT2_Utils.class ->
-    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
-  val add_builtin_fun': SMT2_Utils.class -> term * string -> Context.generic ->
+  val add_builtin_fun: SMT2_Util.class -> (string * typ) * bfunr option bfun -> Context.generic ->
     Context.generic
+  val add_builtin_fun': SMT2_Util.class -> term * string -> Context.generic -> Context.generic
   val add_builtin_fun_ext: (string * typ) * term list bfun ->
     Context.generic -> Context.generic
   val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
@@ -56,7 +55,7 @@
 
 datatype ('a, 'b) kind = Ext of 'a | Int of 'b
 
-type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Utils.dict 
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict 
 
 fun typ_ord ((T, _), (U, _)) =
   let
@@ -69,17 +68,15 @@
   in tord (T, U) end
 
 fun insert_ttab cs T f =
-  SMT2_Utils.dict_map_default (cs, [])
+  SMT2_Util.dict_map_default (cs, [])
     (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
 
-fun merge_ttab ttabp =
-  SMT2_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
+fun merge_ttab ttabp = SMT2_Util.dict_merge (Ord_List.merge typ_ord) ttabp
 
 fun lookup_ttab ctxt ttab T =
   let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
   in
-    get_first (find_first match)
-      (SMT2_Utils.dict_lookup ttab (SMT2_Config.solver_class_of ctxt))
+    get_first (find_first match) (SMT2_Util.dict_lookup ttab (SMT2_Config.solver_class_of ctxt))
   end
 
 type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
@@ -120,8 +117,7 @@
 fun add_builtin_typ cs (T, f, g) =
   Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
 
-fun add_builtin_typ_ext (T, f) =
-  Builtins.map (apfst (insert_ttab SMT2_Utils.basicC T (Ext f)))
+fun add_builtin_typ_ext (T, f) = Builtins.map (apfst (insert_ttab SMT2_Util.basicC T (Ext f)))
 
 fun lookup_builtin_typ ctxt =
   lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
@@ -170,7 +166,7 @@
   in add_builtin_fun cs (c, bfun) end
 
 fun add_builtin_fun_ext ((n, T), f) =
-  Builtins.map (apsnd (insert_btab SMT2_Utils.basicC n T (Ext f)))
+  Builtins.map (apsnd (insert_btab SMT2_Util.basicC n T (Ext f)))
 
 fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
 
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_config.ML
--- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -9,7 +9,7 @@
   (*solver*)
   type solver_info = {
     name: string,
-    class: Proof.context -> SMT2_Utils.class,
+    class: Proof.context -> SMT2_Util.class,
     avail: unit -> bool,
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
@@ -18,7 +18,7 @@
   val available_solvers_of: Proof.context -> string list
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Proof.context -> string
-  val solver_class_of: Proof.context -> SMT2_Utils.class
+  val solver_class_of: Proof.context -> SMT2_Util.class
   val solver_options_of: Proof.context -> string list
 
   (*options*)
@@ -57,9 +57,9 @@
 
 type solver_info = {
   name: string,
-  class: Proof.context -> SMT2_Utils.class,
+  class: Proof.context -> SMT2_Util.class,
   avail: unit -> bool,
-  options: Proof.context -> string list }
+  options: Proof.context -> string list}
 
 (* FIXME just one data slot (record) per program unit *)
 structure Solvers = Generic_Data
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -9,8 +9,7 @@
   val drop_fact_warning: Proof.context -> thm -> unit
   val atomize_conv: Proof.context -> conv
   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
-  val add_extra_norm: SMT2_Utils.class * extra_norm -> Context.generic ->
-    Context.generic
+  val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
   val normalize: (int * (int option * thm)) list -> Proof.context ->
     (int * thm) list * Proof.context
 end
@@ -28,8 +27,7 @@
 (** instantiate elimination rules **)
  
 local
-  val (cpfalse, cfalse) =
-    `SMT2_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
+  val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
 
   fun inst f ct thm =
     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -102,8 +100,7 @@
 in
 
 fun unfold_special_quants_conv ctxt =
-  SMT2_Utils.if_exists_conv (is_some o special_quant)
-    (Conv.top_conv special_quant_conv ctxt)
+  SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
 
 val setup_unfolded_quants =
   fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
@@ -144,8 +141,7 @@
       "must have the same kind: " ^ Syntax.string_of_term ctxt t)
 
   fun check_trigger_conv ctxt ct =
-    if proper_quant false proper_trigger (SMT2_Utils.term_of ct) then
-      Conv.all_conv ct
+    if proper_quant false proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
     else check_trigger_error ctxt (Thm.term_of ct)
 
 
@@ -198,12 +194,10 @@
             Pattern.matches thy (t', u) andalso not (t aconv u))
         in not (Term.exists_subterm some_match u) end
 
-  val pat =
-    SMT2_Utils.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Utils.destT1
-  fun mk_pat ct = Thm.apply (SMT2_Utils.instT' ct pat) ct
+  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
+  fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
 
-  fun mk_clist T = pairself (Thm.cterm_of @{theory})
-    (HOLogic.cons_const T, HOLogic.nil_const T)
+  fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
   val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
@@ -236,20 +230,17 @@
     | has_trigger _ = false
 
   fun try_trigger_conv cv ct =
-    if SMT2_Utils.under_quant has_trigger (SMT2_Utils.term_of ct) then
-      Conv.all_conv ct
+    if SMT2_Util.under_quant has_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
     else Conv.try_conv cv ct
 
   fun infer_trigger_conv ctxt =
     if Config.get ctxt SMT2_Config.infer_triggers then
-      try_trigger_conv
-        (SMT2_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
+      try_trigger_conv (SMT2_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
     else Conv.all_conv
 in
 
 fun trigger_conv ctxt =
-  SMT2_Utils.prop_conv
-    (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
+  SMT2_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
 
 val setup_trigger =
   fold SMT2_Builtin.add_builtin_fun_ext''
@@ -281,8 +272,7 @@
       Syntax.string_of_term ctxt t)
 
   fun check_weight_conv ctxt ct =
-    if SMT2_Utils.under_quant proper_trigger (SMT2_Utils.term_of ct) then
-      Conv.all_conv ct
+    if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
     else check_weight_error ctxt (Thm.term_of ct)
 
 
@@ -304,12 +294,11 @@
   fun add_weight_conv NONE _ = Conv.all_conv
     | add_weight_conv (SOME weight) ctxt =
         let val cv = Conv.rewr_conv (mk_weight_eq weight)
-        in SMT2_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
+        in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end
 in
 
 fun weight_conv weight ctxt = 
-  SMT2_Utils.prop_conv
-    (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
+  SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
 
 val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight}
 
@@ -364,12 +353,11 @@
     "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
 
   fun unfold_conv _ =
-    SMT2_Utils.if_true_conv (is_case_bool o Term.head_of)
-      (expand_head_conv (Conv.rewr_conv thm))
+    SMT2_Util.if_true_conv (is_case_bool o Term.head_of) (expand_head_conv (Conv.rewr_conv thm))
 in
 
 fun rewrite_case_bool_conv ctxt =
-  SMT2_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
+  SMT2_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
 
 val setup_case_bool =
   SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
@@ -409,8 +397,7 @@
 in
 
 fun unfold_abs_min_max_conv ctxt =
-  SMT2_Utils.if_exists_conv (is_some o abs_min_max ctxt)
-    (Conv.top_conv unfold_amm_conv ctxt)
+  SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
   
 val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs
 
@@ -478,7 +465,7 @@
 
   fun mk_number_eq ctxt i lhs =
     let
-      val eq = SMT2_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
+      val eq = SMT2_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
       val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_numeral}
       val tac = HEADGOAL (Simplifier.simp_tac ctxt')
     in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
@@ -500,11 +487,10 @@
   and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
 
   and expand_conv ctxt =
-    SMT2_Utils.if_conv (is_nat_const o Term.head_of)
-      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
-      (int_conv ctxt)
+    SMT2_Util.if_conv (is_nat_const o Term.head_of)
+      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
 
-  and nat_conv ctxt = SMT2_Utils.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
+  and nat_conv ctxt = SMT2_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
 
   val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
 in
@@ -544,13 +530,12 @@
       addsimps @{thms Num.numeral_One minus_zero})
 
   fun norm_num_conv ctxt =
-    SMT2_Utils.if_conv (is_strange_number ctxt)
-      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
+    SMT2_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
+      Conv.no_conv
 in
 
 fun normalize_numerals_conv ctxt =
-  SMT2_Utils.if_exists_conv (is_strange_number ctxt)
-    (Conv.top_sweep_conv norm_num_conv ctxt)
+  SMT2_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt)
 
 end
 
@@ -584,19 +569,18 @@
 
 structure Extra_Norms = Generic_Data
 (
-  type T = extra_norm SMT2_Utils.dict
+  type T = extra_norm SMT2_Util.dict
   val empty = []
   val extend = I
-  fun merge data = SMT2_Utils.dict_merge fst data
+  fun merge data = SMT2_Util.dict_merge fst data
 )
 
-fun add_extra_norm (cs, norm) =
-  Extra_Norms.map (SMT2_Utils.dict_update (cs, norm))
+fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT2_Util.dict_update (cs, norm))
 
 fun apply_extra_norms ctxt ithms =
   let
     val cs = SMT2_Config.solver_class_of ctxt
-    val es = SMT2_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
+    val es = SMT2_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
 
 local
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_real.ML
--- a/src/HOL/Tools/SMT2/smt2_real.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_real.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -21,8 +21,8 @@
 local
   fun real_num _ i = SOME (string_of_int i ^ ".0")
 
-  fun is_linear [t] = SMT2_Utils.is_number t
-    | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u
+  fun is_linear [t] = SMT2_Util.is_number t
+    | is_linear [t, u] = SMT2_Util.is_number t orelse SMT2_Util.is_number u
     | is_linear _ = false
 
   fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -10,7 +10,7 @@
   datatype outcome = Unsat | Sat | Unknown
   type solver_config = {
     name: string,
-    class: Proof.context -> SMT2_Utils.class,
+    class: Proof.context -> SMT2_Util.class,
     avail: unit -> bool,
     command: unit -> string list,
     options: Proof.context -> string list,
@@ -142,7 +142,7 @@
 
 type solver_config = {
   name: string,
-  class: Proof.context -> SMT2_Utils.class,
+  class: Proof.context -> SMT2_Util.class,
   avail: unit -> bool,
   command: unit -> string list,
   options: Proof.context -> string list,
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Tools/SMT2/smt2_setup_solvers.ML
+(*  Title:      HOL/Tools/SMT2/smt2_systems.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Setup SMT solvers.
 *)
 
-signature SMT2_SETUP_SOLVERS =
+signature SMT2_SYSTEMS =
 sig
   datatype z3_non_commercial =
     Z3_Non_Commercial_Unknown |
@@ -14,7 +14,7 @@
   val z3_extensions: bool Config.T
 end
 
-structure SMT2_Setup_Solvers: SMT2_SETUP_SOLVERS =
+structure SMT2_Systems: SMT2_SYSTEMS =
 struct
 
 (* helper functions *)
@@ -168,7 +168,7 @@
   supports_filter = true,
   outcome = z3_on_first_or_last_line,
   cex_parser = SOME Z3_New_Model.parse_counterex,
-  replay = SOME Z3_New_Proof_Replay.replay }
+  replay = SOME Z3_New_Replay.replay }
 
 end
 
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -33,7 +33,7 @@
     assms: (int * thm) list }
 
   (*translation*)
-  val add_config: SMT2_Utils.class * (Proof.context -> config) -> Context.generic -> Context.generic
+  val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
   val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
 end
 
@@ -175,7 +175,7 @@
     in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
 
   fun expf k i T t =
-    let val Ts = drop i (fst (SMT2_Utils.dest_funT k T))
+    let val Ts = drop i (fst (SMT2_Util.dest_funT k T))
     in
       Term.incr_boundvars (length Ts) t
       |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
@@ -256,7 +256,7 @@
   fun apply i t T ts =
     let
       val (ts1, ts2) = chop i ts
-      val (_, U) = SMT2_Utils.dest_funT i T
+      val (_, U) = SMT2_Util.dest_funT i T
     in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
 in
 
@@ -459,7 +459,7 @@
       | _ => raise TERM ("bad SMT term", [t]))
  
     and transs t T ts =
-      let val (Us, U) = SMT2_Utils.dest_funT (length ts) T
+      let val (Us, U) = SMT2_Util.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
         add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
@@ -474,21 +474,21 @@
 
 structure Configs = Generic_Data
 (
-  type T = (Proof.context -> config) SMT2_Utils.dict
+  type T = (Proof.context -> config) SMT2_Util.dict
   val empty = []
   val extend = I
-  fun merge data = SMT2_Utils.dict_merge fst data
+  fun merge data = SMT2_Util.dict_merge fst data
 )
 
-fun add_config (cs, cfg) = Configs.map (SMT2_Utils.dict_update (cs, cfg))
+fun add_config (cs, cfg) = Configs.map (SMT2_Util.dict_update (cs, cfg))
 
 fun get_config ctxt = 
   let val cs = SMT2_Config.solver_class_of ctxt
   in
-    (case SMT2_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of
+    (case SMT2_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of
       SOME cfg => cfg ctxt
     | NONE => error ("SMT: no translation configuration found " ^
-        "for solver class " ^ quote (SMT2_Utils.string_of_class cs)))
+        "for solver class " ^ quote (SMT2_Util.string_of_class cs)))
   end
 
 fun translate ctxt comments ithms =
@@ -498,7 +498,7 @@
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
 
-    val ts1 = map (Envir.beta_eta_contract o SMT2_Utils.prop_of o snd) ithms
+    val ts1 = map (Envir.beta_eta_contract o SMT2_Util.prop_of o snd) ithms
 
     val ((funcs, dtyps, tr_context, ctxt1), ts2) =
       ((empty_tr_context, ctxt), ts1)
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smt2_util.ML
--- a/src/HOL/Tools/SMT2/smt2_util.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_util.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Tools/SMT2/smt2_utils.ML
+(*  Title:      HOL/Tools/SMT2/smt2_util.ML
     Author:     Sascha Boehme, TU Muenchen
 
 General utility functions.
 *)
 
-signature SMT2_UTILS =
+signature SMT2_UTIL =
 sig
   (*basic combinators*)
   val repeat: ('a -> 'a option) -> 'a -> 'a
@@ -61,7 +61,7 @@
   val prop_conv: conv -> conv
 end
 
-structure SMT2_Utils: SMT2_UTILS =
+structure SMT2_Util: SMT2_UTIL =
 struct
 
 (* basic combinators *)
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/smtlib2_interface.ML
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -7,9 +7,8 @@
 
 signature SMTLIB2_INTERFACE =
 sig
-  val smtlib2C: SMT2_Utils.class
-  val add_logic: int * (term list -> string option) -> Context.generic ->
-    Context.generic
+  val smtlib2C: SMT2_Util.class
+  val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
   val translate_config: Proof.context -> SMT2_Translate.config
 end
 
@@ -24,8 +23,8 @@
 local
   fun int_num _ i = SOME (string_of_int i)
 
-  fun is_linear [t] = SMT2_Utils.is_number t
-    | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u
+  fun is_linear [t] = SMT2_Util.is_number t
+    | is_linear [t, u] = SMT2_Util.is_number t orelse SMT2_Util.is_number u
     | is_linear _ = false
 
   fun times _ _ ts =
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_interface.ML
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -6,7 +6,7 @@
 
 signature Z3_NEW_INTERFACE =
 sig
-  val smtlib2_z3C: SMT2_Utils.class
+  val smtlib2_z3C: SMT2_Util.class
 
   datatype sym = Sym of string * sym list
   type mk_builtins = {
@@ -145,26 +145,21 @@
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
-val eq = SMT2_Utils.mk_const_pat @{theory} @{const_name HOL.eq} SMT2_Utils.destT1
-fun mk_eq ct cu = Thm.mk_binop (SMT2_Utils.instT' ct eq) ct cu
+val eq = SMT2_Util.mk_const_pat @{theory} @{const_name HOL.eq} SMT2_Util.destT1
+fun mk_eq ct cu = Thm.mk_binop (SMT2_Util.instT' ct eq) ct cu
 
 val if_term =
-  SMT2_Utils.mk_const_pat @{theory} @{const_name If}
-    (SMT2_Utils.destT1 o SMT2_Utils.destT2)
-fun mk_if cc ct cu =
-  Thm.mk_binop (Thm.apply (SMT2_Utils.instT' ct if_term) cc) ct cu
+  SMT2_Util.mk_const_pat @{theory} @{const_name If} (SMT2_Util.destT1 o SMT2_Util.destT2)
+fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT2_Util.instT' ct if_term) cc) ct
 
-val access =
-  SMT2_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT2_Utils.destT1
-fun mk_access array = Thm.apply (SMT2_Utils.instT' array access) array
+val access = SMT2_Util.mk_const_pat @{theory} @{const_name fun_app} SMT2_Util.destT1
+fun mk_access array = Thm.apply (SMT2_Util.instT' array access) array
 
-val update = SMT2_Utils.mk_const_pat @{theory} @{const_name fun_upd}
-  (Thm.dest_ctyp o SMT2_Utils.destT1)
+val update =
+  SMT2_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT2_Util.destT1)
 fun mk_update array index value =
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
-  in
-    Thm.apply (Thm.mk_binop (SMT2_Utils.instTs cTs update) array index) value
-  end
+  in Thm.apply (Thm.mk_binop (SMT2_Util.instTs cTs update) array index) value end
 
 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
 val add = Thm.cterm_of @{theory} @{const plus (int)}
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_model.ML
--- a/src/HOL/Tools/SMT2/z3_new_model.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_model.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -122,10 +122,8 @@
   | trans_expr T (Value i) = pair (Var (("value", i), T))
   | trans_expr T (Array a) = trans_array T a
   | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
-      let val Ts = fst (SMT2_Utils.dest_funT (length es') (Term.fastype_of t))
-      in
-        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
-      end)
+      let val Ts = fst (SMT2_Util.dest_funT (length es') (Term.fastype_of t))
+      in fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t end)
 
 and trans_array T a =
   let val (dT, rT) = Term.dest_funT T
@@ -164,7 +162,7 @@
 fun translate ((t, k), (e, cs)) =
   let
     val T = Term.fastype_of t
-    val (Us, U) = SMT2_Utils.dest_funT k (Term.fastype_of t)
+    val (Us, U) = SMT2_Util.dest_funT k (Term.fastype_of t)
 
     fun mk_full_def u' pats =
       pats
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,17 +1,17 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof_replay.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay.ML
     Author:     Sascha Boehme, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Z3 proof replay.
 *)
 
-signature Z3_NEW_PROOF_REPLAY =
+signature Z3_NEW_REPLAY =
 sig
   val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
     (int list * Z3_New_Proof.z3_step list) * thm
 end
 
-structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
+structure Z3_New_Replay: Z3_NEW_REPLAY =
 struct
 
 fun params_of t = Term.strip_qnt_vars @{const_name all} t
@@ -21,7 +21,7 @@
     val maxidx = Thm.maxidx_of thm + 1
     val vs = params_of (Thm.prop_of thm)
     val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
-  in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end
+  in Drule.forall_elim_list (map (SMT2_Util.certify ctxt) vars) thm end
 
 fun add_paramTs names t =
   fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
@@ -29,7 +29,7 @@
 fun new_fixes ctxt nTs =
   let
     val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
-    fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T)))
+    fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
   in (ctxt', Symtab.make (map2 mk nTs ns)) end
 
 fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
@@ -56,12 +56,12 @@
 
 fun replay_thm ctxt assumed nthms
     (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
-  if Z3_New_Proof_Methods.is_assumption rule then
+  if Z3_New_Replay_Methods.is_assumption rule then
     (case Inttab.lookup assumed id of
       SOME (_, thm) => thm
-    | NONE => Thm.assume (SMT2_Utils.certify ctxt concl))
+    | NONE => Thm.assume (SMT2_Util.certify ctxt concl))
   else
-    under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
+    under_fixes (Z3_New_Replay_Methods.method_for rule) ctxt
       (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
 
 fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
@@ -77,26 +77,26 @@
     | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
 
   val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
-    remove_fun_app, Z3_New_Proof_Literals.rewrite_true]
+    remove_fun_app, Z3_New_Replay_Literals.rewrite_true]
 
   fun rewrite _ [] = I
     | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
 
   fun lookup_assm assms_net ct =
-    Z3_New_Proof_Tools.net_instances assms_net ct
+    Z3_New_Replay_Util.net_instances assms_net ct
     |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
 in
 
 fun add_asserted outer_ctxt rewrite_rules assms steps ctxt =
   let
-    val eqs = map (rewrite ctxt [Z3_New_Proof_Literals.rewrite_true]) rewrite_rules
+    val eqs = map (rewrite ctxt [Z3_New_Replay_Literals.rewrite_true]) rewrite_rules
     val eqs' = union Thm.eq_thm eqs prep_rules
 
     val assms_net =
       assms
       |> map (apsnd (rewrite ctxt eqs'))
       |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
-      |> Z3_New_Proof_Tools.thm_net_of snd 
+      |> Z3_New_Replay_Util.thm_net_of snd 
 
     fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
 
@@ -117,9 +117,9 @@
 
     fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
         (cx as ((is, thms), (ctxt, ptab))) =
-      if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+      if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
         let
-          val ct = SMT2_Utils.certify ctxt concl
+          val ct = SMT2_Util.certify ctxt concl
           val thm1 =
             Thm.trivial ct
             |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
@@ -154,7 +154,7 @@
 end
 
 fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
-  @{thm reflexive}, Z3_New_Proof_Literals.true_thm]
+  @{thm reflexive}, Z3_New_Replay_Literals.true_thm]
 
 val intro_def_rules = @{lemma
   "(~ P | P) & (P | ~ P)"
@@ -181,7 +181,7 @@
     ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
   let
     val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt
-    val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1
+    val ctxt2 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt1 []) ctxt1
     val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
     val proofs = fold (replay_step ctxt3 assumed) steps assumed
     val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay_literals.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof_literals.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay_literals.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Proof tools related to conjunctions and disjunctions.
 *)
 
-signature Z3_NEW_PROOF_LITERALS =
+signature Z3_NEW_REPLAY_LITERALS =
 sig
   (*literal table*)
   type littab = thm Termtab.table
@@ -30,7 +30,7 @@
   val prove_conj_disj_eq: cterm -> thm
 end
 
-structure Z3_New_Proof_Literals: Z3_NEW_PROOF_LITERALS =
+structure Z3_New_Replay_Literals: Z3_NEW_REPLAY_LITERALS =
 struct
 
 
@@ -39,11 +39,10 @@
 
 type littab = thm Termtab.table
 
-fun make_littab thms =
-  fold (Termtab.update o `SMT2_Utils.prop_of) thms Termtab.empty
+fun make_littab thms = fold (Termtab.update o `SMT2_Util.prop_of) thms Termtab.empty
 
-fun insert_lit thm = Termtab.update (`SMT2_Utils.prop_of thm)
-fun delete_lit thm = Termtab.delete (SMT2_Utils.prop_of thm)
+fun insert_lit thm = Termtab.update (`SMT2_Util.prop_of thm)
+fun delete_lit thm = Termtab.delete (SMT2_Util.prop_of thm)
 fun lookup_lit lits = Termtab.lookup lits
 fun get_first_lit f =
   Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
@@ -91,7 +90,7 @@
 (** explosion of conjunctions and disjunctions **)
 
 local
-  val precomp = Z3_New_Proof_Tools.precompose2
+  val precomp = Z3_New_Replay_Util.precompose2
 
   fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
   val dest_conj1 = precomp destc @{thm conjunct1}
@@ -115,7 +114,7 @@
     | NONE => NONE)
 
   fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
-  val dneg_rule = Z3_New_Proof_Tools.precompose destn @{thm notnotD}
+  val dneg_rule = Z3_New_Replay_Util.precompose destn @{thm notnotD}
 in
 
 (*
@@ -150,7 +149,7 @@
 (*
   extract a literal by applying previously collected rules
 *)
-fun extract_lit thm rules = fold Z3_New_Proof_Tools.compose rules thm
+fun extract_lit thm rules = fold Z3_New_Replay_Util.compose rules thm
 
 
 (*
@@ -162,9 +161,9 @@
     val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
 
     fun explode1 thm =
-      if Termtab.defined tab (SMT2_Utils.prop_of thm) then cons thm
+      if Termtab.defined tab (SMT2_Util.prop_of thm) then cons thm
       else
-        (case dest_rules (SMT2_Utils.prop_of thm) of
+        (case dest_rules (SMT2_Util.prop_of thm) of
           SOME (rule1, rule2) =>
             explode2 rule1 thm #>
             explode2 rule2 thm #>
@@ -173,13 +172,13 @@
 
     and explode2 dest_rule thm =
       if full orelse
-        exists_lit is_conj (Termtab.defined tab) (SMT2_Utils.prop_of thm)
-      then explode1 (Z3_New_Proof_Tools.compose dest_rule thm)
-      else cons (Z3_New_Proof_Tools.compose dest_rule thm)
+        exists_lit is_conj (Termtab.defined tab) (SMT2_Util.prop_of thm)
+      then explode1 (Z3_New_Replay_Util.compose dest_rule thm)
+      else cons (Z3_New_Replay_Util.compose dest_rule thm)
 
     fun explode0 thm =
-      if not is_conj andalso is_dneg (SMT2_Utils.prop_of thm)
-      then [Z3_New_Proof_Tools.compose dneg_rule thm]
+      if not is_conj andalso is_dneg (SMT2_Util.prop_of thm)
+      then [Z3_New_Replay_Util.compose dneg_rule thm]
       else explode1 thm []
 
   in explode0 end
@@ -195,7 +194,7 @@
   fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
   fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
     Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
-    |> Z3_New_Proof_Tools.discharge thm1 |> Z3_New_Proof_Tools.discharge thm2
+    |> Z3_New_Replay_Util.discharge thm1 |> Z3_New_Replay_Util.discharge thm2
 
   fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
 
@@ -219,12 +218,12 @@
   fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
     | dest_disj t = raise TERM ("dest_disj", [t])
 
-  val precomp = Z3_New_Proof_Tools.precompose
+  val precomp = Z3_New_Replay_Util.precompose
   val dnegE = precomp (single o d2 o d1) @{thm notnotD}
   val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
   fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
 
-  val precomp2 = Z3_New_Proof_Tools.precompose2
+  val precomp2 = Z3_New_Replay_Util.precompose2
   fun dni f = apsnd f o Thm.dest_binop o f o d1
   val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
   val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
@@ -243,17 +242,16 @@
 
     fun lookup_rule t =
       (case t of
-        @{const Not} $ (@{const Not} $ t) =>
-          (Z3_New_Proof_Tools.compose dnegI, lookup t)
+        @{const Not} $ (@{const Not} $ t) => (Z3_New_Replay_Util.compose dnegI, lookup t)
       | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
-          (Z3_New_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t))
+          (Z3_New_Replay_Util.compose negIffI, lookup (iff_const $ u $ t))
       | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
           let fun rewr lit = lit COMP @{thm not_sym}
           in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
       | _ =>
           (case as_dneg lookup t of
-            NONE => (Z3_New_Proof_Tools.compose negIffE, as_negIff lookup t)
-          | x => (Z3_New_Proof_Tools.compose dnegE, x)))
+            NONE => (Z3_New_Replay_Util.compose negIffE, as_negIff lookup t)
+          | x => (Z3_New_Replay_Util.compose dnegE, x)))
 
     fun join1 (s, t) =
       (case lookup t of
@@ -286,7 +284,7 @@
   val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
   fun contra_left conj thm =
     let
-      val rules = explode_term conj (SMT2_Utils.prop_of thm)
+      val rules = explode_term conj (SMT2_Util.prop_of thm)
       fun contra_lits (t, rs) =
         (case t of
           @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
@@ -303,9 +301,10 @@
   val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
   fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
 in
+
 fun contradict conj ct =
-  iff_intro (Z3_New_Proof_Tools.under_assumption (contra_left conj) ct)
-    (contra_right ct)
+  iff_intro (Z3_New_Replay_Util.under_assumption (contra_left conj) ct) (contra_right ct)
+
 end
 
 local
@@ -315,8 +314,8 @@
       fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
       fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
 
-      val thm1 = Z3_New_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
-      val thm2 = Z3_New_Proof_Tools.under_assumption (prove l cl o make_tab r) cr
+      val thm1 = Z3_New_Replay_Util.under_assumption (prove r cr o make_tab l) cl
+      val thm2 = Z3_New_Replay_Util.under_assumption (prove l cl o make_tab r) cr
     in iff_intro thm1 thm2 end
 
   datatype conj_disj = CONJ | DISJ | NCON | NDIS
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay_methods.ML
     Author:     Sascha Boehme, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Proof methods for replaying Z3 proofs.
 *)
 
-signature Z3_NEW_PROOF_METHODS =
+signature Z3_NEW_REPLAY_METHODS =
 sig
   (*abstraction*)
   type abs_context = int * term Termtab.table
@@ -53,7 +53,7 @@
   val method_for: Z3_New_Proof.z3_rule -> z3_method
 end
 
-structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS =
+structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
 struct
 
 type z3_method = Proof.context -> thm list -> term -> thm
@@ -90,7 +90,7 @@
 
 fun dest_thm thm = dest_prop (Thm.concl_of thm)
 
-fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t)
+fun certify_prop ctxt t = SMT2_Util.certify ctxt (as_prop t)
 
 fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
   | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
@@ -116,12 +116,12 @@
 
 fun match_instantiate ctxt t thm =
   let
-    val cert = SMT2_Utils.certify ctxt
+    val cert = SMT2_Util.certify ctxt
     val thm' = match_instantiateT ctxt t thm
   in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
 
 fun apply_rule ctxt t =
-  (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of
+  (case Z3_New_Replay_Rules.apply ctxt (certify_prop ctxt t) of
     SOME thm => thm
   | NONE => raise Fail "apply_rule")
 
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay_rules.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,25 +1,23 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof_rules.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay_rules.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Custom rules for Z3 proof replay.
 *)
 
-signature Z3_NEW_PROOF_RULES =
+signature Z3_NEW_REPLAY_RULES =
 sig
   val apply: Proof.context -> cterm -> thm option
 end
 
-structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES =
+structure Z3_New_Replay_Rules: Z3_NEW_REPLAY_RULES =
 struct
 
-val eq = Thm.eq_thm
-
 structure Data = Generic_Data
 (
   type T = thm Net.net
   val empty = Net.empty
   val extend = I
-  val merge = Net.merge eq
+  val merge = Net.merge Thm.eq_thm
 )
 
 fun maybe_instantiate ct thm =
@@ -40,8 +38,8 @@
 
 val prep = `Thm.prop_of
 
-fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
-fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
+fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
 
 val add = Thm.declaration_attribute (Data.map o ins)
 val del = Thm.declaration_attribute (Data.map o del)
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/SMT2/z3_new_replay_util.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_proof_tools.ML
+(*  Title:      HOL/Tools/SMT2/z3_new_replay_util.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Helper functions required for Z3 proof replay.
 *)
 
-signature Z3_NEW_PROOF_TOOLS =
+signature Z3_NEW_REPLAY_UTIL =
 sig
   (*theorem nets*)
   val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
@@ -25,7 +25,7 @@
   val make_simpset: Proof.context -> thm list -> simpset
 end
 
-structure Z3_New_Proof_Tools: Z3_NEW_PROOF_TOOLS =
+structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
 struct
 
 
@@ -63,8 +63,7 @@
 (* proof combinators *)
 
 fun under_assumption f ct =
-  let val ct' = SMT2_Utils.mk_cprop ct
-  in Thm.implies_intr ct' (f (Thm.assume ct')) end
+  let val ct' = SMT2_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
 
 fun discharge p pq = Thm.implies_elim pq p
 
diff -r 99c82a837f8a -r 34bd10a9a2ad src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -122,7 +122,7 @@
            |> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
            |> not (Config.get ctxt smt2_builtins)
               ? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
-                 #> Config.put SMT2_Setup_Solvers.z3_extensions false)
+                 #> Config.put SMT2_Systems.z3_extensions false)
            |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
                 default_max_new_mono_instances