# HG changeset patch
# User wenzelm
# Date 1243789520 -7200
# Node ID 526e149999cc547361a5ff18ff293d5831480439
# Parent  fe786d4633b9fe5e77e0f8eed08e5ff089c9cda0
attempt to eliminate adhoc makestring at runtime (which is not well-defined);

diff -r fe786d4633b9 -r 526e149999cc src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Sun May 31 17:47:04 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Sun May 31 19:05:20 2009 +0200
@@ -320,7 +320,7 @@
 		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
 		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
 		val right = (indexed "C" c)^" "^(string_of_tuple xs)
-		val message = "(\"unresolved lazy call: "^(string_of_int c)^", \"^(makestring x"^(string_of_int (strict_args - 1))^"))"		
+		val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"
 		val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right		
 	    in
 		(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right
diff -r fe786d4633b9 -r 526e149999cc src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Sun May 31 17:47:04 2009 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Sun May 31 19:05:20 2009 +0200
@@ -379,7 +379,11 @@
         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
         val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
         val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
-        val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
+        val _ =
+          if not (null shyps) then
+            raise Compute ("dangling sort hypotheses: " ^
+              commas (map (Syntax.string_of_sort_global thy) shyps))
+          else ()
     in
         Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
     end)));
@@ -610,7 +614,8 @@
             case match_aterms varsubst b' a' of
                 NONE => 
                 let
-                    fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
+                    fun mk s = Syntax.string_of_term_global Pure.thy
+                      (infer_types (naming_of computer) (encoding_of computer) ty s)
                     val left = "computed left side: "^(mk a')
                     val right = "computed right side: "^(mk b')
                 in