added facts_map;
authorwenzelm
Wed Nov 29 04:11:14 2006 +0100 (2006-11-29)
changeset 215817799b1739a51
parent 21580 ff8062cd41e9
child 21582 ac6af184bfb0
added facts_map;
replaced export(_standard)_facts by generalize_facts;
tuned;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Wed Nov 29 04:11:13 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Wed Nov 29 04:11:14 2006 +0100
     1.3 @@ -21,6 +21,9 @@
     1.4      Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
     1.5    type context (*= (string, string, thmref) ctxt*)
     1.6    type context_i (*= (typ, term, thm list) ctxt*)
     1.7 +  val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
     1.8 +   ((string * Attrib.src list) * ('fact * Attrib.src list) list) list ->
     1.9 +   ((string * Attrib.src list) * ('c * Attrib.src list) list) list
    1.10    val map_ctxt: {name: string -> string,
    1.11      var: string * mixfix -> string * mixfix,
    1.12      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
    1.13 @@ -65,10 +68,7 @@
    1.14    val satisfy_facts: witness list ->
    1.15      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.16      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.17 -  val export_facts: Proof.context -> Proof.context ->
    1.18 -    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.19 -    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.20 -  val export_standard_facts: Proof.context -> Proof.context ->
    1.21 +  val generalize_facts: Proof.context -> Proof.context ->
    1.22      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.23      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.24  end;
    1.25 @@ -100,6 +100,8 @@
    1.26  type context = (string, string, thmref) ctxt;
    1.27  type context_i = (typ, term, thm list) ctxt;
    1.28  
    1.29 +fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
    1.30 +
    1.31  fun map_ctxt {name, var, typ, term, fact, attrib} =
    1.32    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
    1.33         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    1.34 @@ -457,35 +459,23 @@
    1.35  
    1.36  fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
    1.37  
    1.38 -fun satisfy_facts witns facts =
    1.39 -  morph_ctxt (satisfy_morphism witns) (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
    1.40 +fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
    1.41  
    1.42  
    1.43  (* generalize type/term parameters *)
    1.44  
    1.45 -local
    1.46 -
    1.47  val maxidx_atts = fold Args.maxidx_values;
    1.48  
    1.49 -fun exp_facts std inner outer facts =
    1.50 +fun generalize_facts inner outer facts =
    1.51    let
    1.52      val thy = ProofContext.theory_of inner;
    1.53      val maxidx =
    1.54        fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
    1.55 -    val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #>
    1.56 -      ((if std then ProofContext.export_standard else ProofContext.export) inner outer);
    1.57 +    val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
    1.58      val exp_term = Drule.term_rule thy (singleton exp_fact);
    1.59      val exp_typ = Logic.type_map exp_term;
    1.60      val morphism =
    1.61        Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
    1.62 -    val Notes (_, facts') = morph_ctxt morphism (Notes ("", facts));
    1.63 -  in facts' end;
    1.64 -
    1.65 -in
    1.66 -
    1.67 -val export_facts = exp_facts false;
    1.68 -val export_standard_facts = exp_facts true;
    1.69 +  in facts_map (morph_ctxt morphism) facts end;
    1.70  
    1.71  end;
    1.72 -
    1.73 -end;