--- a/NEWS Tue Dec 18 02:19:14 2012 +0100
+++ b/NEWS Tue Dec 18 21:59:44 2012 +0100
@@ -102,6 +102,10 @@
*** Pure ***
+* Dropped legacy antiquotations "term_style" and "thm_style", since
+styles may be given as arguments to "term" and "thm" already. Dropped
+legacy styles "prem1" .. "prem19". INCOMPATIBILITY.
+
* Code generation for Haskell: restrict unqualified imports from
Haskell Prelude to a small set of fundamental operations.
--- a/src/Pure/Thy/term_style.ML Tue Dec 18 02:19:14 2012 +0100
+++ b/src/Pure/Thy/term_style.ML Tue Dec 18 21:59:44 2012 +0100
@@ -8,7 +8,6 @@
sig
val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory
val parse: (term -> term) context_parser
- val parse_bare: (term -> term) context_parser
end;
structure Term_Style: TERM_STYLE =
@@ -53,12 +52,6 @@
>> fold I
|| Scan.succeed I));
-val parse_bare = Args.context :|-- (fn ctxt => (legacy_feature "Old-style antiquotation style.";
- Scan.lift Args.liberal_name
- >> (fn name => fst (Args.context_syntax "style"
- (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
- (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
-
(* predefined styles *)
@@ -81,19 +74,6 @@
" in propositon: " ^ Syntax.string_of_term ctxt t)
end);
-fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
- let
- val i_str = string_of_int i;
- val _ = legacy_feature (quote ("prem" ^ i_str)
- ^ " term style encountered; use explicit argument syntax "
- ^ quote ("prem " ^ i_str) ^ " instead.");
- val prems = Logic.strip_imp_prems t;
- in
- if i <= length prems then nth prems (i - 1)
- else error ("Not enough premises for prem" ^ i_str ^
- " in propositon: " ^ Syntax.string_of_term ctxt t)
- end);
-
fun isub_symbols (d :: s :: ss) =
if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
then d :: "\\<^isub>" :: isub_symbols (s :: ss)
@@ -115,25 +95,6 @@
setup "rhs" (style_lhs_rhs snd) #>
setup "prem" style_prem #>
setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup "isub" (Scan.succeed (K isub_term)) #>
- setup "prem1" (style_parm_premise 1) #>
- setup "prem2" (style_parm_premise 2) #>
- setup "prem3" (style_parm_premise 3) #>
- setup "prem4" (style_parm_premise 4) #>
- setup "prem5" (style_parm_premise 5) #>
- setup "prem6" (style_parm_premise 6) #>
- setup "prem7" (style_parm_premise 7) #>
- setup "prem8" (style_parm_premise 8) #>
- setup "prem9" (style_parm_premise 9) #>
- setup "prem10" (style_parm_premise 10) #>
- setup "prem11" (style_parm_premise 11) #>
- setup "prem12" (style_parm_premise 12) #>
- setup "prem13" (style_parm_premise 13) #>
- setup "prem14" (style_parm_premise 14) #>
- setup "prem15" (style_parm_premise 15) #>
- setup "prem16" (style_parm_premise 16) #>
- setup "prem17" (style_parm_premise 17) #>
- setup "prem18" (style_parm_premise 18) #>
- setup "prem19" (style_parm_premise 19)));
+ setup "isub" (Scan.succeed (K isub_term))));
end;
--- a/src/Pure/Thy/thy_output.ML Tue Dec 18 02:19:14 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Dec 18 21:59:44 2012 +0100
@@ -595,11 +595,7 @@
basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
- basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory #>
- basic_entities_style (Binding.name "thm_style")
- (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
- basic_entity (Binding.name "term_style")
- (Term_Style.parse_bare -- Args.term) pretty_term_style));
+ basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory));
end;