# HG changeset patch
# User wenzelm
# Date 1160177474 -7200
# Node ID f26672c248ee979a18f7aca8a9e973bff8e975aa
# Parent  e0223c1bd7e8bb7a8104ca4d9e1cafc2b80ef593
replaced generalize_facts by full export_(standard_)facts;

diff -r e0223c1bd7e8 -r f26672c248ee src/Pure/Isar/element.ML
--- 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;