src/FOLP/simp.ML
changeset 26939 1035c89b4c02
parent 26928 ca87aff1ad2d
child 29265 5b4247055bd7
     1.1 --- a/src/FOLP/simp.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -381,12 +381,12 @@
     1.4  
     1.5  (*print lhs of conclusion of subgoal i*)
     1.6  fun pr_goal_lhs i st =
     1.7 -    writeln (Sign.string_of_term (Thm.theory_of_thm st) 
     1.8 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) 
     1.9               (lhs_of (prepare_goal i st)));
    1.10  
    1.11  (*print conclusion of subgoal i*)
    1.12  fun pr_goal_concl i st =
    1.13 -    writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st)) 
    1.14 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) 
    1.15  
    1.16  (*print subgoals i to j (inclusive)*)
    1.17  fun pr_goals (i,j) st =