src/Pure/Thy/term_style.ML
changeset 43277 1fd31f859fc7
parent 42360 da8817d01e7c
child 50592 a39250169636
     1.1 --- a/src/Pure/Thy/term_style.ML	Wed Jun 08 15:25:44 2011 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Wed Jun 08 15:39:55 2011 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4        >> fold I
     1.5    || Scan.succeed I));
     1.6  
     1.7 -val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
     1.8 +val parse_bare = Args.context :|-- (fn ctxt => (legacy_feature "Old-style antiquotation style.";
     1.9    Scan.lift Args.liberal_name
    1.10    >> (fn name => fst (Args.context_syntax "style"
    1.11         (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    1.12 @@ -84,7 +84,7 @@
    1.13  fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    1.14    let
    1.15      val i_str = string_of_int i;
    1.16 -    val _ = Output.legacy_feature (quote ("prem" ^ i_str)
    1.17 +    val _ = legacy_feature (quote ("prem" ^ i_str)
    1.18        ^ " term style encountered; use explicit argument syntax "
    1.19        ^ quote ("prem " ^ i_str) ^ " instead.");
    1.20      val prems = Logic.strip_imp_prems t;