src/Pure/Isar/element.ML
changeset 21440 807a39221a58
parent 21032 a4b85340d6bd
child 21481 025ab31286d8
     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