notes: proper kind;
authorwenzelm
Tue Nov 21 18:07:37 2006 +0100 (2006-11-21)
changeset 21440807a39221a58
parent 21439 303ec9e9f74f
child 21441 940ef3e85c5a
notes: proper kind;
src/Pure/Isar/element.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Pure/Isar/element.ML	Tue Nov 21 18:07:36 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Nov 21 18:07:37 2006 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4      Constrains of (string * 'typ) list |
     1.5      Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
     1.6      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
     1.7 -    Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
     1.8 +    Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
     1.9    type context (*= (string, string, thmref) ctxt*)
    1.10    type context_i (*= (typ, term, thm list) ctxt*)
    1.11    val map_ctxt: {name: string -> string,
    1.12 @@ -97,7 +97,7 @@
    1.13    Constrains of (string * 'typ) list |
    1.14    Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
    1.15    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.16 -  Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
    1.17 +  Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
    1.18  
    1.19  type context = (string, string, thmref) ctxt;
    1.20  type context_i = (typ, term, thm list) ctxt;
    1.21 @@ -110,7 +110,7 @@
    1.22        ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
    1.23     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    1.24        ((name a, map attrib atts), (term t, map term ps))))
    1.25 -   | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
    1.26 +   | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
    1.27        ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
    1.28  
    1.29  fun map_ctxt_values typ term thm = map_ctxt
    1.30 @@ -133,7 +133,7 @@
    1.31  
    1.32  fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
    1.33    | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
    1.34 -  | facts_of _ (Notes facts) = facts
    1.35 +  | facts_of _ (Notes (_, facts)) = facts
    1.36    | facts_of _ _ = [];
    1.37  
    1.38  
    1.39 @@ -208,7 +208,8 @@
    1.40       | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
    1.41       | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
    1.42       | Defines defs => pretty_items "defines" "and" (map prt_def defs)
    1.43 -     | Notes facts => pretty_items "notes" "and" (map prt_note facts)
    1.44 +     | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
    1.45 +     | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
    1.46    end;
    1.47  
    1.48  
    1.49 @@ -464,7 +465,7 @@
    1.50  fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
    1.51  
    1.52  fun satisfy_facts witns facts =
    1.53 -  satisfy_ctxt witns (Notes facts) |> (fn Notes facts' => facts');
    1.54 +  satisfy_ctxt witns (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
    1.55  
    1.56  
    1.57  (* generalize type/term parameters *)
    1.58 @@ -482,7 +483,7 @@
    1.59        singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer);
    1.60      val exp_term = Drule.term_rule thy exp_thm;
    1.61      val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type;
    1.62 -    val Notes facts' = map_ctxt_values exp_typ exp_term exp_thm (Notes facts);
    1.63 +    val Notes (_, facts') = map_ctxt_values exp_typ exp_term exp_thm (Notes ("", facts));
    1.64    in facts' end;
    1.65  
    1.66  in
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Nov 21 18:07:36 2006 +0100
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 21 18:07:37 2006 +0100
     2.3 @@ -382,7 +382,7 @@
     2.4    $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp))
     2.5      >> Element.Defines ||
     2.6    $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
     2.7 -    >> Element.Notes;
     2.8 +    >> (curry Element.Notes "");
     2.9  
    2.10  fun plus1 test scan =
    2.11    scan -- Scan.repeat ($$$ "+" |-- Scan.unless test (!!! scan)) >> op ::;
     3.1 --- a/src/Pure/Tools/invoke.ML	Tue Nov 21 18:07:36 2006 +0100
     3.2 +++ b/src/Pure/Tools/invoke.ML	Tue Nov 21 18:07:37 2006 +0100
     3.3 @@ -80,7 +80,7 @@
     3.4            ctxt
     3.5            |> ProofContext.sticky_prefix prfx
     3.6            |> ProofContext.qualified_names
     3.7 -          |> (snd o ProofContext.note_thmss_i notes)
     3.8 +          |> (snd o ProofContext.note_thmss_i "" notes)
     3.9            |> ProofContext.restore_naming ctxt
    3.10          end) #>
    3.11        Proof.put_facts NONE #> Seq.single;