--- a/src/ZF/Tools/primrec_package.ML Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sun May 18 15:04:09 2008 +0200
@@ -24,7 +24,7 @@
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
fun primrec_eq_err sign s eq =
- primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
+ primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq);
(* preprocessing of equations *)
@@ -125,8 +125,8 @@
in
if !Ind_Syntax.trace then
writeln ("recursor_rhs = " ^
- Sign.string_of_term thy recursor_rhs ^
- "\nabs = " ^ Sign.string_of_term thy abs)
+ Syntax.string_of_term_global thy recursor_rhs ^
+ "\nabs = " ^ Syntax.string_of_term_global thy abs)
else();
if Logic.occs (fconst, abs) then
primrec_eq_err thy
@@ -152,7 +152,7 @@
in
if !Ind_Syntax.trace then
writeln ("primrec def:\n" ^
- Sign.string_of_term thy def_tm)
+ Syntax.string_of_term_global thy def_tm)
else();
(Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
def_tm)