# HG changeset patch
# User wenzelm
# Date 1154550421 -7200
# Node ID a44096c94b3c790de9509e4ab79fff15b4d5fe04
# Parent  614b7e6c627638b84edaada1a0f5d9ed53e30f99
removed obsolete Drule.frees/vars_of etc.;
simplified Assumption/ProofContext.export;

diff -r 614b7e6c6276 -r a44096c94b3c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Aug 02 22:27:00 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 02 22:27:01 2006 +0200
@@ -127,16 +127,19 @@
 fun legacy_unvarifyT thm =
   let
     val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
-    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (Drule.tvars_of thm);
+    val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
+    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
   in Drule.instantiate' tfrees [] thm end;
 
 fun legacy_unvarify raw_thm =
   let
     val thm = legacy_unvarifyT raw_thm;
     val ct = Thm.cterm_of (Thm.theory_of_thm thm);
-    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (Drule.vars_of thm);
+    val vars = rev (Drule.fold_terms Term.add_vars thm []);
+    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
   in Drule.instantiate' [] frees thm end;
 
+
 (** locale elements and expressions **)
 
 datatype ctxt = datatype Element.ctxt;
@@ -866,8 +869,7 @@
 
 fun axioms_export axs _ hyps =
   Element.satisfy_thm axs
-  #> Drule.implies_intr_list (Library.drop (length axs, hyps))
-  #> Seq.single;
+  #> Drule.implies_intr_list (Library.drop (length axs, hyps));
 
 
 (* NB: derived ids contain only facts at this stage *)