1.1 --- a/src/Pure/Isar/obtain.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4        if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
     1.5      val _ = null bads orelse
     1.6        error ("Result contains obtained parameters: " ^
     1.7 -        space_implode " " (map (ProofContext.string_of_term ctxt) bads));
     1.8 +        space_implode " " (map (Syntax.string_of_term ctxt) bads));
     1.9    in tm end;
    1.10  
    1.11  fun eliminate fix_ctxt rule xs As thm =
    1.12 @@ -217,8 +217,8 @@
    1.13      val thy = ProofContext.theory_of ctxt;
    1.14      val certT = Thm.ctyp_of thy;
    1.15      val cert = Thm.cterm_of thy;
    1.16 -    val string_of_typ = ProofContext.string_of_typ ctxt;
    1.17 -    val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
    1.18 +    val string_of_typ = Syntax.string_of_typ ctxt;
    1.19 +    val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
    1.20  
    1.21      fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
    1.22