src/Pure/codegen.ML
changeset 26939 1035c89b4c02
parent 26931 aa226d8405a8
child 26974 83adc1eaeaab
     1.1 --- a/src/Pure/codegen.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -582,13 +582,13 @@
     1.4  fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
     1.5     (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
     1.6        NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
     1.7 -        Sign.string_of_term thy t)
     1.8 +        Syntax.string_of_term_global thy t)
     1.9      | SOME x => x);
    1.10  
    1.11  fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
    1.12     (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
    1.13        NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
    1.14 -        Sign.string_of_typ thy T)
    1.15 +        Syntax.string_of_typ_global thy T)
    1.16      | SOME x => x);
    1.17  
    1.18  
    1.19 @@ -987,10 +987,10 @@
    1.20          let val T = the_default (the_default (TFree p) default_type)
    1.21            (AList.lookup (op =) tvinsts s)
    1.22          in if Sign.of_sort thy (T, S) then T
    1.23 -          else error ("Type " ^ Sign.string_of_typ thy T ^
    1.24 +          else error ("Type " ^ Syntax.string_of_typ_global thy T ^
    1.25              " to be substituted for variable " ^
    1.26 -            Sign.string_of_typ thy (TFree p) ^ "\ndoes not have sort " ^
    1.27 -            Sign.string_of_sort thy S)
    1.28 +            Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
    1.29 +            Syntax.string_of_sort_global thy S)
    1.30          end))
    1.31        (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
    1.32    in test_term thy quiet size iterations gi' end;