--- a/src/Pure/Isar/element.ML Sat Oct 07 01:31:13 2006 +0200
+++ b/src/Pure/Isar/element.ML Sat Oct 07 01:31:14 2006 +0200
@@ -66,7 +66,10 @@
val satisfy_facts: witness list ->
((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
((string * Attrib.src list) * (thm list * Attrib.src list) list) list
- val generalize_facts: Proof.context -> Proof.context ->
+ val export_facts: Proof.context -> Proof.context ->
+ ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
+ val export_standard_facts: Proof.context -> Proof.context ->
((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
((string * Attrib.src list) * (thm list * Attrib.src list) list) list
end;
@@ -466,17 +469,27 @@
(* generalize type/term parameters *)
+local
+
val maxidx_atts = fold Args.maxidx_values;
-fun generalize_facts inner outer facts =
+fun exp_facts std inner outer facts =
let
val thy = ProofContext.theory_of inner;
val maxidx =
fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
- val gen_thm = Thm.adjust_maxidx_thm maxidx #> singleton (Variable.export inner outer);
- val gen_term = Thm.cterm_of thy #> Drule.mk_term #> gen_thm #> Drule.dest_term #> Thm.term_of;
- val gen_typ = Logic.mk_type #> gen_term #> Logic.dest_type;
- val Notes facts' = map_ctxt_values gen_typ gen_term gen_thm (Notes facts);
+ val exp_thm = Thm.adjust_maxidx_thm maxidx #>
+ 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);
in facts' end;
+in
+
+val export_facts = exp_facts false;
+val export_standard_facts = exp_facts true;
+
end;
+
+end;