# HG changeset patch # User wenzelm # Date 1164128857 -3600 # Node ID 807a39221a58b75ddd5cf737b51fe7dccc0c576e # Parent 303ec9e9f74fc891091adaf0413b7dfc2d1d666c notes: proper kind; diff -r 303ec9e9f74f -r 807a39221a58 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Nov 21 18:07:36 2006 +0100 +++ b/src/Pure/Isar/element.ML Tue Nov 21 18:07:37 2006 +0100 @@ -18,7 +18,7 @@ Constrains of (string * 'typ) list | Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list | Defines of ((string * Attrib.src list) * ('term * 'term list)) list | - Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list + Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list type context (*= (string, string, thmref) ctxt*) type context_i (*= (typ, term, thm list) ctxt*) val map_ctxt: {name: string -> string, @@ -97,7 +97,7 @@ Constrains of (string * 'typ) list | Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list | Defines of ((string * Attrib.src list) * ('term * 'term list)) list | - Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list; + Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list; type context = (string, string, thmref) ctxt; type context_i = (typ, term, thm list) ctxt; @@ -110,7 +110,7 @@ ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => ((name a, map attrib atts), (term t, map term ps)))) - | Notes facts => Notes (facts |> map (fn ((a, atts), bs) => + | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); fun map_ctxt_values typ term thm = map_ctxt @@ -133,7 +133,7 @@ fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs - | facts_of _ (Notes facts) = facts + | facts_of _ (Notes (_, facts)) = facts | facts_of _ _ = []; @@ -208,7 +208,8 @@ | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) | Defines defs => pretty_items "defines" "and" (map prt_def defs) - | Notes facts => pretty_items "notes" "and" (map prt_note facts) + | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts) + | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts) end; @@ -464,7 +465,7 @@ fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns); fun satisfy_facts witns facts = - satisfy_ctxt witns (Notes facts) |> (fn Notes facts' => facts'); + satisfy_ctxt witns (Notes ("", facts)) |> (fn Notes (_, facts') => facts'); (* generalize type/term parameters *) @@ -482,7 +483,7 @@ singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer); val exp_term = Drule.term_rule thy exp_thm; val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type; - val Notes facts' = map_ctxt_values exp_typ exp_term exp_thm (Notes facts); + val Notes (_, facts') = map_ctxt_values exp_typ exp_term exp_thm (Notes ("", facts)); in facts' end; in diff -r 303ec9e9f74f -r 807a39221a58 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Tue Nov 21 18:07:36 2006 +0100 +++ b/src/Pure/Isar/outer_parse.ML Tue Nov 21 18:07:37 2006 +0100 @@ -382,7 +382,7 @@ $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp)) >> Element.Defines || $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) - >> Element.Notes; + >> (curry Element.Notes ""); fun plus1 test scan = scan -- Scan.repeat ($$$ "+" |-- Scan.unless test (!!! scan)) >> op ::; diff -r 303ec9e9f74f -r 807a39221a58 src/Pure/Tools/invoke.ML --- a/src/Pure/Tools/invoke.ML Tue Nov 21 18:07:36 2006 +0100 +++ b/src/Pure/Tools/invoke.ML Tue Nov 21 18:07:37 2006 +0100 @@ -80,7 +80,7 @@ ctxt |> ProofContext.sticky_prefix prfx |> ProofContext.qualified_names - |> (snd o ProofContext.note_thmss_i notes) + |> (snd o ProofContext.note_thmss_i "" notes) |> ProofContext.restore_naming ctxt end) #> Proof.put_facts NONE #> Seq.single;