Variable.import(T): result includes fixed types/terms;

--- a/doc-src/IsarImplementation/Thy/proof.thy	Wed Jul 26 19:23:04 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Wed Jul 26 19:37:41 2006 +0200
@@ -15,7 +15,7 @@
   \begin{mldecls}
   @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
   @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
-  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
+  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\
   @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\

--- a/src/HOL/Tools/datatype_package.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -810,7 +810,7 @@
       ||>> apply_theorems [raw_induction];
     val sign = Theory.sign_of thy1;
 
-    val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction);
+    val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term sign t);

--- a/src/Provers/project_rule.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Provers/project_rule.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -37,7 +37,7 @@
       (case try imp th of
         NONE => (k, th)
       | SOME th' => prems (k + 1) th');
-    val ([rule], ctxt') = Variable.import true [raw_rule] ctxt;
+    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     fun result i =
       rule
       |> proj i
@@ -57,7 +57,7 @@
       (case try conj2 th of
         NONE => k
       | SOME th' => projs (k + 1) th');
-    val ([rule], _) = Variable.import true [raw_rule] ctxt;
+    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
   in projects ctxt (1 upto projs 1 rule) raw_rule end;
 
 end;

--- a/src/Pure/Isar/element.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -219,7 +219,7 @@
     val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     val As = Logic.strip_imp_prems (Thm.term_of prop');
     fun var (x, T) = (ProofContext.revert_skolem ctxt' x, SOME T);
-  in (("", (map var xs, As)), ctxt') end;
+  in (("", (map (var o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
 
 in
 
@@ -231,7 +231,7 @@
     val th = Goal.norm_hhf raw_th;
     val is_elim = ObjectLogic.is_elim th;
 
-    val ([th'], ctxt') = Variable.import true [th] ctxt;
+    val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
     val concl_term = ObjectLogic.drop_judgment thy concl;

--- a/src/Pure/Isar/obtain.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -209,7 +209,7 @@
     val instT =
       fold (Term.add_tvarsT o #2) params []
       |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
-    val (rule' :: terms', ctxt') =
+    val ((_, rule' :: terms'), ctxt') =
       Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
 
     val vars' =

--- a/src/Pure/Isar/rule_cases.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -329,7 +329,7 @@
   | mutual_rule _ [th] = SOME ([0], th)
   | mutual_rule ctxt (ths as th :: _) =
       let
-        val (ths', ctxt') = Variable.import true ths ctxt;
+        val ((_, ths'), ctxt') = Variable.import true ths ctxt;
         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
         val (ns, rls) = split_list (map #2 rules);
       in

--- a/src/Pure/Tools/codegen_theorems.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -581,7 +581,7 @@
     fun cmp_thms (thm1, thm2) =
       not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
     fun unvarify thms =
-      #1 (Variable.import true thms (ProofContext.init thy));
+      #2 (#1 (Variable.import true thms (ProofContext.init thy)));
     val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
   in
     thms

--- a/src/Pure/Tools/invoke.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -63,7 +63,7 @@
       Seq.map (Proof.map_context (fn ctxt =>
         let
           val ([res_types, res_params, res_prems], ctxt'') =
-            fold_burrow (Variable.import false) results ctxt';
+            fold_burrow (apfst snd oo Variable.import false) results ctxt';
 
           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
           val params'' = map (Thm.term_of o Drule.dest_term) res_params;

--- a/src/Pure/tactic.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/tactic.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -136,7 +136,7 @@
 fun rule_by_tactic tac rl =
   let
     val ctxt = Variable.thm_context rl;
-    val ([st], ctxt') = Variable.import true [rl] ctxt;
+    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])