added formal comment arguments almost everywhere (still ignored);
authorwenzelm
Tue May 25 20:23:30 1999 +0200 (1999-05-25)
changeset 6728b51b25db7bc6
parent 6727 c8dba1da73cc
child 6729 b6e167580a32
added formal comment arguments almost everywhere (still ignored);
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue May 25 20:22:41 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue May 25 20:23:30 1999 +0200
     1.3 @@ -13,70 +13,104 @@
     1.4    val add_section: Comment.text -> theory -> theory
     1.5    val add_subsection: Comment.text -> theory -> theory
     1.6    val add_subsubsection: Comment.text -> theory -> theory
     1.7 -  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
     1.8 -  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
     1.9 -  val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    1.10 -  val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    1.11 -  val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
    1.12 -  val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
    1.13 +  val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
    1.14 +  val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
    1.15 +  val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
    1.16 +  val add_classrel_i: (class * class) * Comment.text -> theory -> theory
    1.17 +  val add_defsort: xsort * Comment.text -> theory -> theory
    1.18 +  val add_defsort_i: sort * Comment.text -> theory -> theory
    1.19 +  val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
    1.20 +  val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
    1.21 +    -> theory -> theory
    1.22 +  val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
    1.23 +    -> theory -> theory
    1.24 +  val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory
    1.25 +  val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
    1.26 +  val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
    1.27 +  val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
    1.28 +  val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory
    1.29 +  val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list
    1.30 +    -> theory -> theory
    1.31 +  val add_modesyntax_i: string * bool -> ((bstring * typ * mixfix) * Comment.text) list
    1.32 +    -> theory -> theory
    1.33 +  val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
    1.34 +  val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
    1.35 +  val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
    1.36 +  val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
    1.37 +    -> theory -> theory
    1.38 +  val add_defs: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
    1.39 +  val add_defs_i: (((bstring * term) * theory attribute list) * Comment.text) list
    1.40 +    -> theory -> theory
    1.41 +  val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list
    1.42 +    -> theory -> theory
    1.43 +  val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list
    1.44 +    -> theory -> theory
    1.45    val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
    1.46    val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
    1.47 -  val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    1.48 -    -> theory -> theory
    1.49 -  val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    1.50 +  val have_theorems: ((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text
    1.51      -> theory -> theory
    1.52 -  val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    1.53 +  val have_theorems_i: ((bstring * theory attribute list) * (thm * theory attribute list) list)
    1.54 +    * Comment.text -> theory -> theory
    1.55 +  val have_lemmas: ((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text
    1.56      -> theory -> theory
    1.57 -  val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    1.58 -    -> theory -> theory
    1.59 -  val have_facts: (string * Args.src list) * (string * Args.src list) list
    1.60 +  val have_lemmas_i: ((bstring * theory attribute list) * (thm * theory attribute list) list)
    1.61 +    * Comment.text -> theory -> theory
    1.62 +  val have_facts: ((string * Args.src list) * (string * Args.src list) list) * Comment.text
    1.63      -> ProofHistory.T -> ProofHistory.T
    1.64 -  val have_facts_i: (string * Proof.context attribute list) *
    1.65 -    (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    1.66 -  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    1.67 -  val from_facts_i: (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    1.68 -  val chain: ProofHistory.T -> ProofHistory.T
    1.69 -  val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    1.70 -  val fix_i: (string * typ) list -> ProofHistory.T -> ProofHistory.T
    1.71 -  val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
    1.72 -  val match_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
    1.73 -  val theorem: string -> Args.src list -> string * string list
    1.74 +  val have_facts_i: ((string * Proof.context attribute list) *
    1.75 +    (thm * Proof.context attribute list) list) * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.76 +  val from_facts: (string * Args.src list) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.77 +  val from_facts_i: (thm * Proof.context attribute list) list * Comment.text
    1.78 +    -> ProofHistory.T -> ProofHistory.T
    1.79 +  val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.80 +  val fix: (string * string option) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.81 +  val fix_i: (string * typ) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.82 +  val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.83 +  val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.84 +  val theorem: (bstring * Args.src list * (string * string list)) * Comment.text
    1.85 +    -> bool -> theory -> ProofHistory.T
    1.86 +  val theorem_i: (bstring * theory attribute list * (term * term list)) * Comment.text
    1.87      -> bool -> theory -> ProofHistory.T
    1.88 -  val theorem_i: bstring -> theory attribute list -> term * term list
    1.89 +  val lemma: (bstring * Args.src list * (string * string list)) * Comment.text
    1.90      -> bool -> theory -> ProofHistory.T
    1.91 -  val lemma: string -> Args.src list -> string * string list
    1.92 +  val lemma_i: (bstring * theory attribute list * (term * term list)) * Comment.text
    1.93      -> bool -> theory -> ProofHistory.T
    1.94 -  val lemma_i: bstring -> theory attribute list -> term * term list
    1.95 -    -> bool -> theory -> ProofHistory.T
    1.96 -  val assume: string -> Args.src list -> (string * string list) list
    1.97 +  val assume: (string * Args.src list * (string * string list) list) * Comment.text
    1.98 +    -> ProofHistory.T -> ProofHistory.T
    1.99 +  val assume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
   1.100      -> ProofHistory.T -> ProofHistory.T
   1.101 -  val assume_i: string -> Proof.context attribute list -> (term * term list) list
   1.102 +  val show: (string * Args.src list * (string * string list)) * Comment.text
   1.103 +    -> ProofHistory.T -> ProofHistory.T
   1.104 +  val show_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
   1.105      -> ProofHistory.T -> ProofHistory.T
   1.106 -  val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
   1.107 -  val show_i: string -> Proof.context attribute list -> term * term list
   1.108 +  val have: (string * Args.src list * (string * string list)) * Comment.text
   1.109      -> ProofHistory.T -> ProofHistory.T
   1.110 -  val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
   1.111 -  val have_i: string -> Proof.context attribute list -> term * term list
   1.112 +  val have_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
   1.113 +    -> ProofHistory.T -> ProofHistory.T
   1.114 +  val thus: (string * Args.src list * (string * string list)) * Comment.text
   1.115      -> ProofHistory.T -> ProofHistory.T
   1.116 -  val thus: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
   1.117 -  val thus_i: string -> Proof.context attribute list -> term * term list
   1.118 +  val thus_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
   1.119      -> ProofHistory.T -> ProofHistory.T
   1.120 -  val hence: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
   1.121 -  val hence_i: string -> Proof.context attribute list -> term * term list
   1.122 +  val hence: (string * Args.src list * (string * string list)) * Comment.text
   1.123 +    -> ProofHistory.T -> ProofHistory.T
   1.124 +  val hence_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
   1.125      -> ProofHistory.T -> ProofHistory.T
   1.126    val begin_block: ProofHistory.T -> ProofHistory.T
   1.127    val next_block: ProofHistory.T -> ProofHistory.T
   1.128    val end_block: ProofHistory.T -> ProofHistory.T
   1.129    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
   1.130    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
   1.131 -  val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
   1.132 +  val proof: Comment.interest * (Method.text * Comment.interest) option
   1.133 +    -> ProofHistory.T -> ProofHistory.T
   1.134    val kill_proof: ProofHistory.T -> theory
   1.135 -  val global_qed_with: bstring option * Args.src list option -> Method.text option
   1.136 +  val global_qed_with: bstring option * Args.src list option
   1.137 +    -> (Method.text * Comment.interest) option
   1.138      -> Toplevel.transition -> Toplevel.transition
   1.139 -  val global_qed_with_i: bstring option * theory attribute list option -> Method.text option
   1.140 +  val global_qed_with_i: bstring option * theory attribute list option
   1.141 +    -> (Method.text * Comment.interest) option
   1.142      -> Toplevel.transition -> Toplevel.transition
   1.143 -  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   1.144 -  val terminal_proof: Method.text -> Toplevel.transition -> Toplevel.transition
   1.145 +  val qed: (Method.text * Comment.interest) option -> Toplevel.transition -> Toplevel.transition
   1.146 +  val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
   1.147    val immediate_proof: Toplevel.transition -> Toplevel.transition
   1.148    val default_proof: Toplevel.transition -> Toplevel.transition
   1.149    val use_mltext: string -> theory option -> theory option
   1.150 @@ -88,7 +122,7 @@
   1.151    val typed_print_translation: string -> theory -> theory
   1.152    val print_ast_translation: string -> theory -> theory
   1.153    val token_translation: string -> theory -> theory
   1.154 -  val add_oracle: bstring * string -> theory -> theory
   1.155 +  val add_oracle: (bstring * string) * Comment.text -> theory -> theory
   1.156    val begin_theory: string -> string list -> (string * bool) list -> theory
   1.157    val end_theory: theory -> theory
   1.158    val theory: string * string list * (string * bool) list
   1.159 @@ -103,9 +137,9 @@
   1.160  
   1.161  (** derived theory and proof operations **)
   1.162  
   1.163 -(* formal comments *)   (* FIXME dummy *)
   1.164 +(* formal comments *)
   1.165  
   1.166 -fun add_text _ thy = thy;
   1.167 +fun add_text comment thy = thy;
   1.168  fun add_title title author date thy = thy;
   1.169  val add_chapter = add_text;
   1.170  val add_section = add_text;
   1.171 @@ -113,26 +147,50 @@
   1.172  val add_subsubsection = add_text;
   1.173  
   1.174  
   1.175 +(* signature and syntax *)
   1.176 +
   1.177 +val add_classes = Theory.add_classes o Comment.ignore;
   1.178 +val add_classes_i = Theory.add_classes_i o Comment.ignore;
   1.179 +val add_classrel = Theory.add_classrel o single o Comment.ignore;
   1.180 +val add_classrel_i = Theory.add_classrel_i o single o Comment.ignore;
   1.181 +val add_defsort = Theory.add_defsort o Comment.ignore;
   1.182 +val add_defsort_i = Theory.add_defsort_i o Comment.ignore;
   1.183 +val add_nonterminals = Theory.add_nonterminals o map Comment.ignore;
   1.184 +val add_tyabbrs = Theory.add_tyabbrs o map Comment.ignore;
   1.185 +val add_tyabbrs_i = Theory.add_tyabbrs_i o map Comment.ignore;
   1.186 +val add_arities = Theory.add_arities o map Comment.ignore;
   1.187 +val add_arities_i = Theory.add_arities_i o map Comment.ignore;
   1.188 +val add_typedecl = PureThy.add_typedecls o single o Comment.ignore;
   1.189 +val add_consts = Theory.add_consts o map Comment.ignore;
   1.190 +val add_consts_i = Theory.add_consts_i o map Comment.ignore;
   1.191 +fun add_modesyntax mode = Theory.add_modesyntax mode o map Comment.ignore;
   1.192 +fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
   1.193 +val add_trrules = Theory.add_trrules o map Comment.ignore;
   1.194 +val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
   1.195 +
   1.196 +
   1.197 +
   1.198  (* axioms and defs *)
   1.199  
   1.200  fun add_axms f args thy =
   1.201    f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
   1.202  
   1.203 -val add_axioms = add_axms PureThy.add_axioms;
   1.204 -val add_axioms_i = PureThy.add_axioms_i;
   1.205 -val add_defs = add_axms PureThy.add_defs;
   1.206 -val add_defs_i = PureThy.add_defs_i;
   1.207 +val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore;
   1.208 +val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore;
   1.209 +val add_defs = add_axms PureThy.add_defs o map Comment.ignore;
   1.210 +val add_defs_i = PureThy.add_defs_i o map Comment.ignore;
   1.211  
   1.212  
   1.213  (* constdefs *)
   1.214  
   1.215  fun gen_add_constdefs consts defs args thy =
   1.216    thy
   1.217 -  |> consts (map fst args)
   1.218 -  |> defs (map (fn ((c, _, mx), s) => ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
   1.219 +  |> consts (map (Comment.ignore o fst) args)
   1.220 +  |> defs (map (fn (((c, _, mx), _), (s, _)) =>
   1.221 +    (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
   1.222  
   1.223 -val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
   1.224 -val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
   1.225 +fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args;
   1.226 +fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args;
   1.227  
   1.228  
   1.229  (* theorems *)
   1.230 @@ -155,62 +213,60 @@
   1.231  
   1.232  fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs);
   1.233  fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs);
   1.234 -val have_theorems = #1 oo global_have_thmss (PureThy.have_thmss o Some);
   1.235 -val have_theorems_i = #1 oo have_thmss_i (PureThy.have_thmss o Some);
   1.236 -val have_lemmas = #1 oo global_have_thmss (have_lemss o Some);
   1.237 -val have_lemmas_i = #1 oo have_thmss_i (have_lemss o Some);
   1.238 -val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss;
   1.239 -val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss;
   1.240 +val have_theorems = #1 oo (global_have_thmss (PureThy.have_thmss o Some) o Comment.ignore);
   1.241 +val have_theorems_i = #1 oo (have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore);
   1.242 +val have_lemmas = #1 oo (global_have_thmss (have_lemss o Some) o Comment.ignore);
   1.243 +val have_lemmas_i = #1 oo (have_thmss_i (have_lemss o Some) o Comment.ignore);
   1.244 +val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss o Comment.ignore;
   1.245 +val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss o Comment.ignore;
   1.246  
   1.247  
   1.248  (* forward chaining *)
   1.249  
   1.250 -val from_facts =
   1.251 -  ProofHistory.apply o (Proof.chain oo curry (local_have_thmss Proof.have_thmss) ("", []));
   1.252 +fun gen_from_facts f = ProofHistory.apply o (Proof.chain oo curry (f Proof.have_thmss) ("", []));
   1.253  
   1.254 -val from_facts_i =
   1.255 -  ProofHistory.apply o (Proof.chain oo curry (have_thmss_i Proof.have_thmss) ("", []));
   1.256 -
   1.257 -val chain = ProofHistory.apply Proof.chain;
   1.258 +val from_facts = gen_from_facts local_have_thmss o Comment.ignore;
   1.259 +val from_facts_i = gen_from_facts have_thmss_i o Comment.ignore;
   1.260 +fun chain comment_ignore = ProofHistory.apply Proof.chain;
   1.261  
   1.262  
   1.263  (* context *)
   1.264  
   1.265 -val fix = ProofHistory.apply o Proof.fix;
   1.266 -val fix_i = ProofHistory.apply o Proof.fix_i;
   1.267 -val match_bind = ProofHistory.apply o Proof.match_bind;
   1.268 -val match_bind_i = ProofHistory.apply o Proof.match_bind_i;
   1.269 +val fix = ProofHistory.apply o Proof.fix o Comment.ignore;
   1.270 +val fix_i = ProofHistory.apply o Proof.fix_i o Comment.ignore;
   1.271 +val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
   1.272 +val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
   1.273  
   1.274  
   1.275  (* statements *)
   1.276  
   1.277 -fun global_statement f name src s int thy =
   1.278 +fun global_statement f (name, src, s) int thy =
   1.279    ProofHistory.init (Toplevel.undo_limit int)
   1.280      (f name (map (Attrib.global_attribute thy) src) s thy);
   1.281  
   1.282 -fun global_statement_i f name atts t int thy =
   1.283 +fun global_statement_i f (name, atts, t) int thy =
   1.284    ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
   1.285  
   1.286 -fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state =>
   1.287 +fun local_statement do_open f g (name, src, s) = ProofHistory.apply_cond_open do_open (fn state =>
   1.288    f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
   1.289  
   1.290 -fun local_statement_i do_open f g name atts t =
   1.291 +fun local_statement_i do_open f g (name, atts, t) =
   1.292    ProofHistory.apply_cond_open do_open (f name atts t o g);
   1.293  
   1.294 -val theorem   = global_statement Proof.theorem;
   1.295 -val theorem_i = global_statement_i Proof.theorem_i;
   1.296 -val lemma     = global_statement Proof.lemma;
   1.297 -val lemma_i   = global_statement_i Proof.lemma_i;
   1.298 -val assume    = local_statement false Proof.assume I;
   1.299 -val assume_i  = local_statement_i false Proof.assume_i I;
   1.300 -val show      = local_statement true Proof.show I;
   1.301 -val show_i    = local_statement_i true Proof.show_i I;
   1.302 -val have      = local_statement true Proof.have I;
   1.303 -val have_i    = local_statement_i true Proof.have_i I;
   1.304 -val thus      = local_statement true Proof.show Proof.chain;
   1.305 -val thus_i    = local_statement_i true Proof.show_i Proof.chain;
   1.306 -val hence     = local_statement true Proof.have Proof.chain;
   1.307 -val hence_i   = local_statement_i true Proof.have_i Proof.chain;
   1.308 +val theorem   = global_statement Proof.theorem o Comment.ignore;
   1.309 +val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
   1.310 +val lemma     = global_statement Proof.lemma o Comment.ignore;
   1.311 +val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
   1.312 +val assume    = local_statement false Proof.assume I o Comment.ignore;
   1.313 +val assume_i  = local_statement_i false Proof.assume_i I o Comment.ignore;
   1.314 +val show      = local_statement true Proof.show I o Comment.ignore;
   1.315 +val show_i    = local_statement_i true Proof.show_i I o Comment.ignore;
   1.316 +val have      = local_statement true Proof.have I o Comment.ignore;
   1.317 +val have_i    = local_statement_i true Proof.have_i I o Comment.ignore;
   1.318 +val thus      = local_statement true Proof.show Proof.chain o Comment.ignore;
   1.319 +val thus_i    = local_statement_i true Proof.show_i Proof.chain o Comment.ignore;
   1.320 +val hence     = local_statement true Proof.have Proof.chain o Comment.ignore;
   1.321 +val hence_i   = local_statement_i true Proof.have_i Proof.chain o Comment.ignore;
   1.322  
   1.323  
   1.324  (* blocks *)
   1.325 @@ -224,16 +280,24 @@
   1.326  
   1.327  val tac = ProofHistory.applys o Method.tac;
   1.328  val then_tac = ProofHistory.applys o Method.then_tac;
   1.329 -val proof = ProofHistory.applys o Method.proof;
   1.330 +
   1.331 +val proof =
   1.332 +  ProofHistory.applys o Method.proof o apsome Comment.ignore_interest o Comment.ignore_interest';
   1.333  
   1.334  
   1.335  (* local endings *)
   1.336  
   1.337 -val local_qed = Toplevel.proof' o (ProofHistory.applys_close oo Method.local_qed);
   1.338 +val local_qed =
   1.339 +  Toplevel.proof' o (ProofHistory.applys_close oo Method.local_qed)
   1.340 +    o apsome Comment.ignore_interest;
   1.341 +
   1.342  val local_terminal_proof =
   1.343 -  Toplevel.proof' o (ProofHistory.applys_close oo Method.local_terminal_proof);
   1.344 +  Toplevel.proof' o (ProofHistory.applys_close oo Method.local_terminal_proof)
   1.345 +    o Comment.ignore_interest;
   1.346 +
   1.347  val local_immediate_proof =
   1.348    Toplevel.proof' (ProofHistory.applys_close o Method.local_immediate_proof);
   1.349 +
   1.350  val local_default_proof =
   1.351    Toplevel.proof' (ProofHistory.applys_close o Method.local_default_proof);
   1.352  
   1.353 @@ -252,25 +316,25 @@
   1.354        [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   1.355    in Pretty.writeln prt_result; thy end);
   1.356  
   1.357 -fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state =
   1.358 +fun gen_global_qed_with prep_att (alt_name, raw_atts) meth state =
   1.359    let
   1.360      val thy = Proof.theory_of state;
   1.361      val alt_atts = apsome (map (prep_att thy)) raw_atts;
   1.362 -  in Method.global_qed alt_name alt_atts opt_text state end;
   1.363 +  in Method.global_qed alt_name alt_atts (apsome Comment.ignore_interest meth) state end;
   1.364  
   1.365  val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
   1.366  val global_qed_with_i = global_result oo gen_global_qed_with (K I);
   1.367  val global_qed = global_qed_with (None, None);
   1.368  
   1.369 -val global_terminal_proof = global_result o Method.global_terminal_proof;
   1.370 +val global_terminal_proof = global_result o Method.global_terminal_proof o Comment.ignore_interest;
   1.371  val global_immediate_proof = global_result Method.global_immediate_proof;
   1.372  val global_default_proof = global_result Method.global_default_proof;
   1.373  
   1.374  
   1.375  (* common endings *)
   1.376  
   1.377 -fun qed opt_text = local_qed opt_text o global_qed opt_text;
   1.378 -fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;
   1.379 +fun qed meth = local_qed meth o global_qed meth;
   1.380 +fun terminal_proof meth = local_terminal_proof meth o global_terminal_proof meth;
   1.381  val immediate_proof = local_immediate_proof o global_immediate_proof;
   1.382  val default_proof = local_default_proof o global_default_proof;
   1.383  
   1.384 @@ -318,7 +382,7 @@
   1.385  
   1.386  (* add_oracle *)
   1.387  
   1.388 -fun add_oracle (name, txt) =
   1.389 +fun add_oracle ((name, txt), comment_ignore) =
   1.390    use_let
   1.391      "oracle: bstring * (Sign.sg * Object.T -> term)"
   1.392      "Theory.add_oracle oracle"