--- 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