--- a/src/FOLP/simp.ML Sat May 17 23:53:20 2008 +0200
+++ b/src/FOLP/simp.ML Sun May 18 15:04:09 2008 +0200
@@ -381,12 +381,12 @@
(*print lhs of conclusion of subgoal i*)
fun pr_goal_lhs i st =
- writeln (Sign.string_of_term (Thm.theory_of_thm st)
+ writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
(lhs_of (prepare_goal i st)));
(*print conclusion of subgoal i*)
fun pr_goal_concl i st =
- writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st))
+ writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
(*print subgoals i to j (inclusive)*)
fun pr_goals (i,j) st =