1.1 --- a/src/Pure/Isar/proof.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -465,7 +465,7 @@
     1.4    let
     1.5      val thy = theory_of state;
     1.6      val ctxt = context_of state;
     1.7 -    val string_of_term = ProofContext.string_of_term ctxt;
     1.8 +    val string_of_term = Syntax.string_of_term ctxt;
     1.9      val string_of_thm = ProofContext.string_of_thm ctxt;
    1.10  
    1.11      val ngoals = Thm.nprems_of goal;