--- 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
--- 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