# HG changeset patch
# User boehmes
# Date 1294389708 -3600
# Node ID a31c451183e62b3202122d3908f2cbd2a67b66dd
# Parent  272fe1f37b6577f0b554bec21acd520133bd3a27
avoid ML structure aliases (especially single-letter abbreviations)

diff -r 272fe1f37b65 -r a31c451183e6 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Fri Jan 07 09:26:27 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Jan 07 09:41:48 2011 +0100
@@ -12,9 +12,6 @@
 structure SMT_Real: SMT_REAL =
 struct
 
-structure U = SMT_Utils
-structure B = SMT_Builtin
-
 
 (* SMT-LIB logic *)
 
@@ -27,12 +24,10 @@
 (* SMT-LIB and Z3 built-ins *)
 
 local
-  val smtlibC = SMTLIB_Interface.smtlibC
-
   fun real_num _ i = SOME (string_of_int i ^ ".0")
 
-  fun is_linear [t] = U.is_number t
-    | is_linear [t, u] = U.is_number t orelse U.is_number u
+  fun is_linear [t] = SMT_Utils.is_number t
+    | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u
     | is_linear _ = false
 
   fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
@@ -42,17 +37,20 @@
 in
 
 val setup_builtins =
-  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
-  fold (B.add_builtin_fun' smtlibC) [
+  SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
+    (@{typ real}, K (SOME "Real"), real_num) #>
+  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
     (@{const less (real)}, "<"),
     (@{const less_eq (real)}, "<="),
     (@{const uminus (real)}, "~"),
     (@{const plus (real)}, "+"),
     (@{const minus (real)}, "-") ] #>
-  B.add_builtin_fun SMTLIB_Interface.smtlibC
+  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
     (Term.dest_Const @{const times (real)}, times) #>
-  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #>
-  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
+  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
+    (@{const times (real)}, "*") #>
+  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
+    (@{const divide (real)}, "/")
 
 end
 
diff -r 272fe1f37b65 -r a31c451183e6 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Fri Jan 07 09:26:27 2011 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML	Fri Jan 07 09:41:48 2011 +0100
@@ -12,8 +12,6 @@
 structure SMT_Word: SMT_WORD =
 struct
 
-structure B = SMT_Builtin
-
 
 (* utilities *)
 
@@ -71,7 +69,7 @@
 
   fun add_word_fun f (t, n) =
     let val c as (m, _) = Term.dest_Const t
-    in B.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
+    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
 
   fun hd2 xs = hd (tl xs)
 
@@ -127,7 +125,7 @@
 in
 
 val setup_builtins =
-  B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
+  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   fold (add_word_fun if_fixed_all) [
     (@{term "uminus :: 'a::len word => _"}, "bvneg"),
     (@{term "plus :: 'a::len word => _"}, "bvadd"),