1.1 --- a/src/Pure/Thy/term_style.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -55,14 +55,14 @@
     1.4        (Logic.strip_imp_concl t)
     1.5    in
     1.6      case concl of (_ $ l $ r) => (l, r)
     1.7 -    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
     1.8 +    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
     1.9    end;
    1.10  
    1.11  fun style_parm_premise i ctxt t =
    1.12    let val prems = Logic.strip_imp_prems t in
    1.13      if i <= length prems then nth prems (i - 1)
    1.14      else error ("Not enough premises for prem" ^ string_of_int i ^
    1.15 -      " in propositon: " ^ ProofContext.string_of_term ctxt t)
    1.16 +      " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.17    end;
    1.18  
    1.19  val _ = Context.add_setup