1.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Apr 03 19:24:11 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Apr 03 19:24:13 2007 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4    \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
     1.5    \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
     1.6    \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
     1.7 -  \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
     1.8 +  \indexml{Variable.import-thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
     1.9  \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
    1.10    \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
    1.11    \end{mldecls}
    1.12 @@ -150,7 +150,7 @@
    1.13    with \verb|Variable.polymorphic|: here the given terms are detached
    1.14    from the context as far as possible.
    1.15  
    1.16 -  \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
    1.17 +  \item \verb|Variable.import_thms|~\isa{open\ thms\ ctxt} invents fixed
    1.18    type and term variables for the schematic ones occurring in \isa{thms}.  The \isa{open} flag indicates whether the fixed names
    1.19    should be accessible to the user, otherwise newly introduced names
    1.20    are marked as ``internal'' (\secref{sec:names}).

     2.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Tue Apr 03 19:24:11 2007 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Tue Apr 03 19:24:13 2007 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4    @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
     2.5    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
     2.6    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     2.7 -  @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     2.8 +  @{index_ML Variable.import_thms: "bool -> thm list -> Proof.context ->
     2.9    ((ctyp list * cterm list) * thm list) * Proof.context"} \\
    2.10    @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
    2.11    \end{mldecls}
    2.12 @@ -133,7 +133,7 @@
    2.13    with @{ML Variable.polymorphic}: here the given terms are detached
    2.14    from the context as far as possible.
    2.15  
    2.16 -  \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
    2.17 +  \item @{ML Variable.import_thms}~@{text "open thms ctxt"} invents fixed
    2.18    type and term variables for the schematic ones occurring in @{text
    2.19    "thms"}.  The @{text "open"} flag indicates whether the fixed names
    2.20    should be accessible to the user, otherwise newly introduced names

     3.1 --- a/src/HOL/ex/reflection.ML	Tue Apr 03 19:24:11 2007 +0200
     3.2 +++ b/src/HOL/ex/reflection.ML	Tue Apr 03 19:24:13 2007 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  				|> fst |> strip_comb |> fst
     3.5     val thy = ProofContext.theory_of ctxt
     3.6     val cert = Thm.cterm_of thy
     3.7 -   val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
     3.8 +   val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
     3.9     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    3.10     fun add_fterms (t as t1 $ t2) = 
    3.11         if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t

     4.1 --- a/src/Provers/project_rule.ML	Tue Apr 03 19:24:11 2007 +0200
     4.2 +++ b/src/Provers/project_rule.ML	Tue Apr 03 19:24:13 2007 +0200
     4.3 @@ -37,7 +37,7 @@
     4.4        (case try imp th of
     4.5          NONE => (k, th)
     4.6        | SOME th' => prems (k + 1) th');
     4.7 -    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     4.8 +    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
     4.9      fun result i =
    4.10        rule
    4.11        |> proj i
    4.12 @@ -57,7 +57,7 @@
    4.13        (case try conj2 th of
    4.14          NONE => k
    4.15        | SOME th' => projs (k + 1) th');
    4.16 -    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
    4.17 +    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
    4.18    in projects ctxt (1 upto projs 1 rule) raw_rule end;
    4.19  
    4.20  end;

     5.1 --- a/src/Pure/Isar/attrib.ML	Tue Apr 03 19:24:11 2007 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Tue Apr 03 19:24:13 2007 +0200
     5.3 @@ -254,7 +254,7 @@
     5.4  fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x;
     5.5  
     5.6  fun no_vars x = no_args (Thm.rule_attribute (fn ctxt => fn th =>
     5.7 -  let val ((_, [th']), _) = Variable.import true [th] (Context.proof_of ctxt)
     5.8 +  let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt)
     5.9    in th' end)) x;
    5.10  
    5.11  fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;

     6.1 --- a/src/Pure/Isar/element.ML	Tue Apr 03 19:24:11 2007 +0200
     6.2 +++ b/src/Pure/Isar/element.ML	Tue Apr 03 19:24:13 2007 +0200
     6.3 @@ -249,7 +249,7 @@
     6.4      val th = MetaSimplifier.norm_hhf raw_th;
     6.5      val is_elim = ObjectLogic.is_elim th;
     6.6  
     6.7 -    val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
     6.8 +    val ((_, [th']), ctxt') = Variable.import_thms true [th] ctxt;
     6.9      val prop = Thm.prop_of th';
    6.10      val (prems, concl) = Logic.strip_horn prop;
    6.11      val concl_term = ObjectLogic.drop_judgment thy concl;

     7.1 --- a/src/Pure/Isar/local_defs.ML	Tue Apr 03 19:24:11 2007 +0200
     7.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Apr 03 19:24:13 2007 +0200
     7.3 @@ -124,7 +124,7 @@
     7.4        (case filter_out is_trivial raw_eqs of
     7.5          [] => th
     7.6        | eqs =>
     7.7 -          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
     7.8 +          let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
     7.9            in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
    7.10  
    7.11  in

     8.1 --- a/src/Pure/Isar/obtain.ML	Tue Apr 03 19:24:11 2007 +0200
     8.2 +++ b/src/Pure/Isar/obtain.ML	Tue Apr 03 19:24:13 2007 +0200
     8.3 @@ -82,7 +82,7 @@
     8.4      val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
     8.5        error "Conclusion in obtained context must be object-logic judgment";
     8.6  
     8.7 -    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
     8.8 +    val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt;
     8.9      val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
    8.10    in
    8.11      ((Drule.implies_elim_list thm' (map Thm.assume prems)
    8.12 @@ -198,7 +198,7 @@
    8.13        | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
    8.14  
    8.15      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
    8.16 -    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    8.17 +    val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt;
    8.18      val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    8.19      val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
    8.20      val (prems, ctxt'') =
    8.21 @@ -251,7 +251,7 @@
    8.22        |> Thm.forall_intr (cert (Free thesis_var))
    8.23        |> Thm.instantiate (instT, []);
    8.24  
    8.25 -    val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
    8.26 +    val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt;
    8.27      val vars' =
    8.28        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
    8.29        (map snd vars @ replicate (length ys) NoSyn);

     9.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Apr 03 19:24:11 2007 +0200
     9.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue Apr 03 19:24:13 2007 +0200
     9.3 @@ -330,7 +330,7 @@
     9.4    | mutual_rule _ [th] = SOME ([0], th)
     9.5    | mutual_rule ctxt (ths as th :: _) =
     9.6        let
     9.7 -        val ((_, ths'), ctxt') = Variable.import true ths ctxt;
     9.8 +        val ((_, ths'), ctxt') = Variable.import_thms true ths ctxt;
     9.9          val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
    9.10          val (ns, rls) = split_list (map #2 rules);
    9.11        in

    10.1 --- a/src/Pure/Tools/invoke.ML	Tue Apr 03 19:24:11 2007 +0200
    10.2 +++ b/src/Pure/Tools/invoke.ML	Tue Apr 03 19:24:13 2007 +0200
    10.3 @@ -63,7 +63,7 @@
    10.4        Proof.map_context (fn ctxt =>
    10.5          let
    10.6            val ([res_types, res_params, res_prems], ctxt'') =
    10.7 -            fold_burrow (apfst snd oo Variable.import false) results ctxt';
    10.8 +            fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';
    10.9  
   10.10            val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
   10.11            val params'' = map (Thm.term_of o Drule.dest_term) res_params;

    11.1 --- a/src/Pure/subgoal.ML	Tue Apr 03 19:24:11 2007 +0200
    11.2 +++ b/src/Pure/subgoal.ML	Tue Apr 03 19:24:13 2007 +0200
    11.3 @@ -30,7 +30,7 @@
    11.4  fun focus ctxt i st =
    11.5    let
    11.6      val ((schematics, [st']), ctxt') =
    11.7 -      Variable.import true [MetaSimplifier.norm_hhf_protect st] ctxt;
    11.8 +      Variable.import_thms true [MetaSimplifier.norm_hhf_protect st] ctxt;
    11.9      val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
   11.10      val asms = Drule.strip_imp_prems goal;
   11.11      val concl = Drule.strip_imp_concl goal;

    12.1 --- a/src/Pure/tactic.ML	Tue Apr 03 19:24:11 2007 +0200
    12.2 +++ b/src/Pure/tactic.ML	Tue Apr 03 19:24:13 2007 +0200
    12.3 @@ -118,7 +118,7 @@
    12.4  fun rule_by_tactic tac rl =
    12.5    let
    12.6      val ctxt = Variable.thm_context rl;
    12.7 -    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
    12.8 +    val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
    12.9    in
   12.10      (case Seq.pull (tac st) of
   12.11        NONE => raise THM ("rule_by_tactic", 0, [rl])

    13.1 --- a/src/Pure/variable.ML	Tue Apr 03 19:24:11 2007 +0200
    13.2 +++ b/src/Pure/variable.ML	Tue Apr 03 19:24:13 2007 +0200
    13.3 @@ -50,7 +50,7 @@
    13.4    val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
    13.5    val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
    13.6    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
    13.7 -  val import: bool -> thm list -> Proof.context ->
    13.8 +  val import_thms: bool -> thm list -> Proof.context ->
    13.9      ((ctyp list * cterm list) * thm list) * Proof.context
   13.10    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   13.11    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   13.12 @@ -392,7 +392,7 @@
   13.13      val (insts, ctxt') = import_inst is_open ts ctxt;
   13.14    in (Proofterm.instantiate insts prf, ctxt') end;
   13.15  
   13.16 -fun import is_open ths ctxt =
   13.17 +fun import_thms is_open ths ctxt =
   13.18    let
   13.19      val thy = ProofContext.theory_of ctxt;
   13.20      val cert = Thm.cterm_of thy;
   13.21 @@ -411,7 +411,7 @@
   13.22    in exp ctxt' ctxt (f ctxt' ths') end;
   13.23  
   13.24  val tradeT = gen_trade importT exportT;
   13.25 -val trade = gen_trade (import true) export;
   13.26 +val trade = gen_trade (import_thms true) export;
   13.27  
   13.28  
   13.29  (* focus on outermost parameters *)