src/FOLP/simp.ML

         val params = rev (Logic.strip_params subgi)
     in variants_abs (params, Logic.strip_assums_concl subgi) end;
 
 (*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 =
     if i>j then ()
     else (pr_goal_concl i st;  pr_goals (i+1,j) st);