src/Pure/Thy/term_style.ML
changeset 24920 2a45e400fdad
parent 23655 d2d1138e0ddc
child 26435 bdce320cd426
--- a/src/Pure/Thy/term_style.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Thy/term_style.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -55,14 +55,14 @@
       (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => (l, r)
-    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
+    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
   end;
 
 fun style_parm_premise i ctxt t =
   let val prems = Logic.strip_imp_prems t in
     if i <= length prems then nth prems (i - 1)
     else error ("Not enough premises for prem" ^ string_of_int i ^
-      " in propositon: " ^ ProofContext.string_of_term ctxt t)
+      " in propositon: " ^ Syntax.string_of_term ctxt t)
   end;
 
 val _ = Context.add_setup