src/Pure/Isar/element.ML
changeset 20886 f26672c248ee
parent 20548 8ef25fe585a8
child 21032 a4b85340d6bd
     1.1 --- a/src/Pure/Isar/element.ML	Sat Oct 07 01:31:13 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sat Oct 07 01:31:14 2006 +0200
     1.3 @@ -66,7 +66,10 @@
     1.4    val satisfy_facts: witness list ->
     1.5      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     1.6      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
     1.7 -  val generalize_facts: Proof.context -> Proof.context ->
     1.8 +  val export_facts: Proof.context -> Proof.context ->
     1.9 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.10 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.11 +  val export_standard_facts: Proof.context -> Proof.context ->
    1.12      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.13      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.14  end;
    1.15 @@ -466,17 +469,27 @@
    1.16  
    1.17  (* generalize type/term parameters *)
    1.18  
    1.19 +local
    1.20 +
    1.21  val maxidx_atts = fold Args.maxidx_values;
    1.22  
    1.23 -fun generalize_facts inner outer facts =
    1.24 +fun exp_facts std inner outer facts =
    1.25    let
    1.26      val thy = ProofContext.theory_of inner;
    1.27      val maxidx =
    1.28        fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
    1.29 -    val gen_thm = Thm.adjust_maxidx_thm maxidx #> singleton (Variable.export inner outer);
    1.30 -    val gen_term = Thm.cterm_of thy #> Drule.mk_term #> gen_thm #> Drule.dest_term #> Thm.term_of;
    1.31 -    val gen_typ = Logic.mk_type #> gen_term #> Logic.dest_type;
    1.32 -    val Notes facts' = map_ctxt_values gen_typ gen_term gen_thm (Notes facts);
    1.33 +    val exp_thm = Thm.adjust_maxidx_thm maxidx #>
    1.34 +      singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer);
    1.35 +    val exp_term = Drule.term_rule thy exp_thm;
    1.36 +    val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type;
    1.37 +    val Notes facts' = map_ctxt_values exp_typ exp_term exp_thm (Notes facts);
    1.38    in facts' end;
    1.39  
    1.40 +in
    1.41 +
    1.42 +val export_facts = exp_facts false;
    1.43 +val export_standard_facts = exp_facts true;
    1.44 +
    1.45  end;
    1.46 +
    1.47 +end;