avoid ML structure aliases (especially single-letter abbreviations)
authorboehmes
Fri Jan 07 09:41:48 2011 +0100 (2011-01-07)
changeset 41439a31c451183e6
parent 41438 272fe1f37b65
child 41440 3e0fc4a54ca1
avoid ML structure aliases (especially single-letter abbreviations)
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Word/Tools/smt_word.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Fri Jan 07 09:26:27 2011 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Jan 07 09:41:48 2011 +0100
     1.3 @@ -12,9 +12,6 @@
     1.4  structure SMT_Real: SMT_REAL =
     1.5  struct
     1.6  
     1.7 -structure U = SMT_Utils
     1.8 -structure B = SMT_Builtin
     1.9 -
    1.10  
    1.11  (* SMT-LIB logic *)
    1.12  
    1.13 @@ -27,12 +24,10 @@
    1.14  (* SMT-LIB and Z3 built-ins *)
    1.15  
    1.16  local
    1.17 -  val smtlibC = SMTLIB_Interface.smtlibC
    1.18 -
    1.19    fun real_num _ i = SOME (string_of_int i ^ ".0")
    1.20  
    1.21 -  fun is_linear [t] = U.is_number t
    1.22 -    | is_linear [t, u] = U.is_number t orelse U.is_number u
    1.23 +  fun is_linear [t] = SMT_Utils.is_number t
    1.24 +    | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u
    1.25      | is_linear _ = false
    1.26  
    1.27    fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
    1.28 @@ -42,17 +37,20 @@
    1.29  in
    1.30  
    1.31  val setup_builtins =
    1.32 -  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    1.33 -  fold (B.add_builtin_fun' smtlibC) [
    1.34 +  SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
    1.35 +    (@{typ real}, K (SOME "Real"), real_num) #>
    1.36 +  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
    1.37      (@{const less (real)}, "<"),
    1.38      (@{const less_eq (real)}, "<="),
    1.39      (@{const uminus (real)}, "~"),
    1.40      (@{const plus (real)}, "+"),
    1.41      (@{const minus (real)}, "-") ] #>
    1.42 -  B.add_builtin_fun SMTLIB_Interface.smtlibC
    1.43 +  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
    1.44      (Term.dest_Const @{const times (real)}, times) #>
    1.45 -  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #>
    1.46 -  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    1.47 +  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
    1.48 +    (@{const times (real)}, "*") #>
    1.49 +  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
    1.50 +    (@{const divide (real)}, "/")
    1.51  
    1.52  end
    1.53  
     2.1 --- a/src/HOL/Word/Tools/smt_word.ML	Fri Jan 07 09:26:27 2011 +0100
     2.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Fri Jan 07 09:41:48 2011 +0100
     2.3 @@ -12,8 +12,6 @@
     2.4  structure SMT_Word: SMT_WORD =
     2.5  struct
     2.6  
     2.7 -structure B = SMT_Builtin
     2.8 -
     2.9  
    2.10  (* utilities *)
    2.11  
    2.12 @@ -71,7 +69,7 @@
    2.13  
    2.14    fun add_word_fun f (t, n) =
    2.15      let val c as (m, _) = Term.dest_Const t
    2.16 -    in B.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
    2.17 +    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
    2.18  
    2.19    fun hd2 xs = hd (tl xs)
    2.20  
    2.21 @@ -127,7 +125,7 @@
    2.22  in
    2.23  
    2.24  val setup_builtins =
    2.25 -  B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
    2.26 +  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
    2.27    fold (add_word_fun if_fixed_all) [
    2.28      (@{term "uminus :: 'a::len word => _"}, "bvneg"),
    2.29      (@{term "plus :: 'a::len word => _"}, "bvadd"),