renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);

--- a/doc-src/IsarImplementation/Thy/Proof.thy	Wed Jun 24 20:52:49 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Wed Jun 24 21:28:02 2009 +0200
@@ -93,7 +93,7 @@
   @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
   @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
-  @{index_ML Variable.import_thms: "bool -> thm list -> Proof.context ->
+  @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
   ((ctyp list * cterm list) * thm list) * Proof.context"} \\
   @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
   \end{mldecls}
@@ -132,7 +132,7 @@
   with @{ML Variable.polymorphic}: here the given terms are detached
   from the context as far as possible.
 
-  \item @{ML Variable.import_thms}~@{text "open thms ctxt"} invents fixed
+  \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
   type and term variables for the schematic ones occurring in @{text
   "thms"}.  The @{text "open"} flag indicates whether the fixed names
   should be accessible to the user, otherwise newly introduced names

--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Wed Jun 24 20:52:49 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Wed Jun 24 21:28:02 2009 +0200
@@ -111,7 +111,7 @@
   \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
-  \indexdef{}{ML}{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+  \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
 \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
   \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   \end{mldecls}
@@ -149,7 +149,7 @@
   with \verb|Variable.polymorphic|: here the given terms are detached
   from the context as far as possible.
 
-  \item \verb|Variable.import_thms|~\isa{open\ thms\ ctxt} invents fixed
+  \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
   type and term variables for the schematic ones occurring in \isa{thms}.  The \isa{open} flag indicates whether the fixed names
   should be accessible to the user, otherwise newly introduced names
   are marked as ``internal'' (\secref{sec:names}).

--- a/doc-src/more_antiquote.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/doc-src/more_antiquote.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -81,7 +81,7 @@
 fun no_vars ctxt thm =
   let
     val ctxt' = Variable.set_body false ctxt;
-    val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
+    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
   in thm end;
 
 fun pretty_code_thm src ctxt raw_const =

--- a/src/HOL/Library/reflection.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -34,7 +34,7 @@
      |> fst |> strip_comb |> fst
    val thy = ProofContext.theory_of ctxt
    val cert = Thm.cterm_of thy
-   val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
+   val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    fun add_fterms (t as t1 $ t2) =
        if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t

--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -385,7 +385,7 @@
 fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   let
     val ((_, [induct']), _) =
-      Variable.importT_thms [induct] (Variable.thm_context induct);
+      Variable.importT [induct] (Variable.thm_context induct);
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Syntax.string_of_term_global thy t);

--- a/src/HOL/Tools/res_axioms.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -269,7 +269,7 @@
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
 fun to_nnf th ctxt0 =
   let val th1 = th |> transform_elim |> zero_var_indexes
-      val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0
+      val ((_,[th2]),ctxt) = Variable.import true [th1] ctxt0
       val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
   in  (th3, ctxt)  end;
 

--- a/src/HOL/Tools/transfer_data.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/HOL/Tools/transfer_data.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -54,7 +54,7 @@
 
 fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
  let 
-  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import_thms true (map Drule.mk_term [a0, D0]) ctxt0)
+  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
   val (aT,bT) = 
      let val T = typ_of (ctyp_of_term a) 
      in (Term.range_type T, Term.domain_type T)

--- a/src/Pure/Isar/attrib.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -265,7 +265,7 @@
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
     val ctxt = Variable.set_body false (Context.proof_of context);
-    val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
+    val ((_, [th']), _) = Variable.import true [th] ctxt;
   in th' end);
 
 val eta_long =

--- a/src/Pure/Isar/class.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/class.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -75,7 +75,7 @@
     (* assm_intro *)
     fun prove_assm_intro thm =
       let
-        val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
+        val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
         val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
         val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
       in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;

--- a/src/Pure/Isar/element.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -225,7 +225,7 @@
     val th = MetaSimplifier.norm_hhf raw_th;
     val is_elim = ObjectLogic.is_elim th;
 
-    val ((_, [th']), ctxt') = Variable.import_thms true [th] (Variable.set_body false ctxt);
+    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false 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/local_defs.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -170,7 +170,7 @@
       (case filter_out is_trivial raw_eqs of
         [] => th
       | eqs =>
-          let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
+          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
           in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
 
 in

--- a/src/Pure/Isar/obtain.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -79,7 +79,7 @@
     val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 
-    val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt;
+    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
     val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
   in
     ((Drule.implies_elim_list thm' (map Thm.assume prems)
@@ -196,7 +196,7 @@
       | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
 
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
-    val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt;
+    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
@@ -249,7 +249,7 @@
       |> Thm.forall_intr (cert (Free thesis_var))
       |> Thm.instantiate (instT, []);
 
-    val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt;
+    val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =
       map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
       (map snd vars @ replicate (length ys) NoSyn);

--- a/src/Pure/Isar/rule_cases.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -333,7 +333,7 @@
   | mutual_rule _ [th] = SOME ([0], th)
   | mutual_rule ctxt (ths as th :: _) =
       let
-        val ((_, ths'), ctxt') = Variable.import_thms 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/subgoal.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/subgoal.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -29,7 +29,7 @@
 fun focus ctxt i st =
   let
     val ((schematics, [st']), ctxt') =
-      Variable.import_thms true [Simplifier.norm_hhf_protect st] ctxt;
+      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
     val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
     val asms = Drule.strip_imp_prems goal;
     val concl = Drule.strip_imp_concl goal;

--- a/src/Pure/tactic.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/tactic.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -91,7 +91,7 @@
 fun rule_by_tactic tac rl =
   let
     val ctxt = Variable.thm_context rl;
-    val ((_, [st]), ctxt') = Variable.import_thms 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])

--- a/src/Pure/variable.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/variable.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -51,9 +51,9 @@
     (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
-  val import_thms: bool -> thm list -> Proof.context ->
+  val import: bool -> thm list -> Proof.context ->
     ((ctyp list * cterm list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -424,7 +424,7 @@
   let val (inst, ctxt') = import_inst is_open ts ctxt
   in (map (TermSubst.instantiate inst) ts, ctxt') end;
 
-fun importT_thms ths ctxt =
+fun importT ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
@@ -439,7 +439,7 @@
     val (insts, ctxt') = import_inst is_open ts ctxt;
   in (Proofterm.instantiate insts prf, ctxt') end;
 
-fun import_thms is_open ths ctxt =
+fun import is_open ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
@@ -457,8 +457,8 @@
   let val ((_, ths'), ctxt') = imp ths ctxt
   in exp ctxt' ctxt (f ctxt' ths') end;
 
-val tradeT = gen_trade importT_thms exportT;
-val trade = gen_trade (import_thms true) export;
+val tradeT = gen_trade importT exportT;
+val trade = gen_trade (import true) export;
 
 
 (* focus on outermost parameters *)

--- a/src/Tools/project_rule.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Tools/project_rule.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -39,7 +39,7 @@
       (case try imp th of
         NONE => (k, th)
       | SOME th' => prems (k + 1) th');
-    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
+    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     fun result i =
       rule
       |> proj i
@@ -59,7 +59,7 @@
       (case try conj2 th of
         NONE => k
       | SOME th' => projs (k + 1) th');
-    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
+    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
   in projects ctxt (1 upto projs 1 rule) raw_rule end;
 
 end;