renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);
1.1 --- a/doc-src/IsarImplementation/Thy/Proof.thy Wed Jun 24 20:52:49 2009 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Wed Jun 24 21:28:02 2009 +0200
1.3 @@ -93,7 +93,7 @@
1.4 @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
1.5 @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
1.6 @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
1.7 - @{index_ML Variable.import_thms: "bool -> thm list -> Proof.context ->
1.8 + @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
1.9 ((ctyp list * cterm list) * thm list) * Proof.context"} \\
1.10 @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
1.11 \end{mldecls}
1.12 @@ -132,7 +132,7 @@
1.13 with @{ML Variable.polymorphic}: here the given terms are detached
1.14 from the context as far as possible.
1.15
1.16 - \item @{ML Variable.import_thms}~@{text "open thms ctxt"} invents fixed
1.17 + \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
1.18 type and term variables for the schematic ones occurring in @{text
1.19 "thms"}. The @{text "open"} flag indicates whether the fixed names
1.20 should be accessible to the user, otherwise newly introduced names
2.1 --- a/doc-src/IsarImplementation/Thy/document/Proof.tex Wed Jun 24 20:52:49 2009 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Wed Jun 24 21:28:02 2009 +0200
2.3 @@ -111,7 +111,7 @@
2.4 \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
2.5 \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
2.6 \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
2.7 - \indexdef{}{ML}{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
2.8 + \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
2.9 \verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
2.10 \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
2.11 \end{mldecls}
2.12 @@ -149,7 +149,7 @@
2.13 with \verb|Variable.polymorphic|: here the given terms are detached
2.14 from the context as far as possible.
2.15
2.16 - \item \verb|Variable.import_thms|~\isa{open\ thms\ ctxt} invents fixed
2.17 + \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
2.18 type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names
2.19 should be accessible to the user, otherwise newly introduced names
2.20 are marked as ``internal'' (\secref{sec:names}).
3.1 --- a/doc-src/more_antiquote.ML Wed Jun 24 20:52:49 2009 +0200
3.2 +++ b/doc-src/more_antiquote.ML Wed Jun 24 21:28:02 2009 +0200
3.3 @@ -81,7 +81,7 @@
3.4 fun no_vars ctxt thm =
3.5 let
3.6 val ctxt' = Variable.set_body false ctxt;
3.7 - val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
3.8 + val ((_, [thm]), _) = Variable.import true [thm] ctxt';
3.9 in thm end;
3.10
3.11 fun pretty_code_thm src ctxt raw_const =
4.1 --- a/src/HOL/Library/reflection.ML Wed Jun 24 20:52:49 2009 +0200
4.2 +++ b/src/HOL/Library/reflection.ML Wed Jun 24 21:28:02 2009 +0200
4.3 @@ -34,7 +34,7 @@
4.4 |> fst |> strip_comb |> fst
4.5 val thy = ProofContext.theory_of ctxt
4.6 val cert = Thm.cterm_of thy
4.7 - val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
4.8 + val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
4.9 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
4.10 fun add_fterms (t as t1 $ t2) =
4.11 if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
5.1 --- a/src/HOL/Tools/Datatype/datatype.ML Wed Jun 24 20:52:49 2009 +0200
5.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Jun 24 21:28:02 2009 +0200
5.3 @@ -385,7 +385,7 @@
5.4 fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
5.5 let
5.6 val ((_, [induct']), _) =
5.7 - Variable.importT_thms [induct] (Variable.thm_context induct);
5.8 + Variable.importT [induct] (Variable.thm_context induct);
5.9
5.10 fun err t = error ("Ill-formed predicate in induction rule: " ^
5.11 Syntax.string_of_term_global thy t);
6.1 --- a/src/HOL/Tools/res_axioms.ML Wed Jun 24 20:52:49 2009 +0200
6.2 +++ b/src/HOL/Tools/res_axioms.ML Wed Jun 24 21:28:02 2009 +0200
6.3 @@ -269,7 +269,7 @@
6.4 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
6.5 fun to_nnf th ctxt0 =
6.6 let val th1 = th |> transform_elim |> zero_var_indexes
6.7 - val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0
6.8 + val ((_,[th2]),ctxt) = Variable.import true [th1] ctxt0
6.9 val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
6.10 in (th3, ctxt) end;
6.11
7.1 --- a/src/HOL/Tools/transfer_data.ML Wed Jun 24 20:52:49 2009 +0200
7.2 +++ b/src/HOL/Tools/transfer_data.ML Wed Jun 24 21:28:02 2009 +0200
7.3 @@ -54,7 +54,7 @@
7.4
7.5 fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
7.6 let
7.7 - val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import_thms true (map Drule.mk_term [a0, D0]) ctxt0)
7.8 + val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
7.9 val (aT,bT) =
7.10 let val T = typ_of (ctyp_of_term a)
7.11 in (Term.range_type T, Term.domain_type T)
8.1 --- a/src/Pure/Isar/attrib.ML Wed Jun 24 20:52:49 2009 +0200
8.2 +++ b/src/Pure/Isar/attrib.ML Wed Jun 24 21:28:02 2009 +0200
8.3 @@ -265,7 +265,7 @@
8.4 val no_vars = Thm.rule_attribute (fn context => fn th =>
8.5 let
8.6 val ctxt = Variable.set_body false (Context.proof_of context);
8.7 - val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
8.8 + val ((_, [th']), _) = Variable.import true [th] ctxt;
8.9 in th' end);
8.10
8.11 val eta_long =
9.1 --- a/src/Pure/Isar/class.ML Wed Jun 24 20:52:49 2009 +0200
9.2 +++ b/src/Pure/Isar/class.ML Wed Jun 24 21:28:02 2009 +0200
9.3 @@ -75,7 +75,7 @@
9.4 (* assm_intro *)
9.5 fun prove_assm_intro thm =
9.6 let
9.7 - val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
9.8 + val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
9.9 val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
9.10 val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
9.11 in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
10.1 --- a/src/Pure/Isar/element.ML Wed Jun 24 20:52:49 2009 +0200
10.2 +++ b/src/Pure/Isar/element.ML Wed Jun 24 21:28:02 2009 +0200
10.3 @@ -225,7 +225,7 @@
10.4 val th = MetaSimplifier.norm_hhf raw_th;
10.5 val is_elim = ObjectLogic.is_elim th;
10.6
10.7 - val ((_, [th']), ctxt') = Variable.import_thms true [th] (Variable.set_body false ctxt);
10.8 + val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
10.9 val prop = Thm.prop_of th';
10.10 val (prems, concl) = Logic.strip_horn prop;
10.11 val concl_term = ObjectLogic.drop_judgment thy concl;
11.1 --- a/src/Pure/Isar/local_defs.ML Wed Jun 24 20:52:49 2009 +0200
11.2 +++ b/src/Pure/Isar/local_defs.ML Wed Jun 24 21:28:02 2009 +0200
11.3 @@ -170,7 +170,7 @@
11.4 (case filter_out is_trivial raw_eqs of
11.5 [] => th
11.6 | eqs =>
11.7 - let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
11.8 + let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
11.9 in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
11.10
11.11 in
12.1 --- a/src/Pure/Isar/obtain.ML Wed Jun 24 20:52:49 2009 +0200
12.2 +++ b/src/Pure/Isar/obtain.ML Wed Jun 24 21:28:02 2009 +0200
12.3 @@ -79,7 +79,7 @@
12.4 val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
12.5 error "Conclusion in obtained context must be object-logic judgment";
12.6
12.7 - val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt;
12.8 + val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
12.9 val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
12.10 in
12.11 ((Drule.implies_elim_list thm' (map Thm.assume prems)
12.12 @@ -196,7 +196,7 @@
12.13 | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
12.14
12.15 val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
12.16 - val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt;
12.17 + val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
12.18 val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
12.19 val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
12.20 val (prems, ctxt'') =
12.21 @@ -249,7 +249,7 @@
12.22 |> Thm.forall_intr (cert (Free thesis_var))
12.23 |> Thm.instantiate (instT, []);
12.24
12.25 - val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt;
12.26 + val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
12.27 val vars' =
12.28 map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
12.29 (map snd vars @ replicate (length ys) NoSyn);
13.1 --- a/src/Pure/Isar/rule_cases.ML Wed Jun 24 20:52:49 2009 +0200
13.2 +++ b/src/Pure/Isar/rule_cases.ML Wed Jun 24 21:28:02 2009 +0200
13.3 @@ -333,7 +333,7 @@
13.4 | mutual_rule _ [th] = SOME ([0], th)
13.5 | mutual_rule ctxt (ths as th :: _) =
13.6 let
13.7 - val ((_, ths'), ctxt') = Variable.import_thms true ths ctxt;
13.8 + val ((_, ths'), ctxt') = Variable.import true ths ctxt;
13.9 val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
13.10 val (ns, rls) = split_list (map #2 rules);
13.11 in
14.1 --- a/src/Pure/subgoal.ML Wed Jun 24 20:52:49 2009 +0200
14.2 +++ b/src/Pure/subgoal.ML Wed Jun 24 21:28:02 2009 +0200
14.3 @@ -29,7 +29,7 @@
14.4 fun focus ctxt i st =
14.5 let
14.6 val ((schematics, [st']), ctxt') =
14.7 - Variable.import_thms true [Simplifier.norm_hhf_protect st] ctxt;
14.8 + Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
14.9 val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
14.10 val asms = Drule.strip_imp_prems goal;
14.11 val concl = Drule.strip_imp_concl goal;
15.1 --- a/src/Pure/tactic.ML Wed Jun 24 20:52:49 2009 +0200
15.2 +++ b/src/Pure/tactic.ML Wed Jun 24 21:28:02 2009 +0200
15.3 @@ -91,7 +91,7 @@
15.4 fun rule_by_tactic tac rl =
15.5 let
15.6 val ctxt = Variable.thm_context rl;
15.7 - val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
15.8 + val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
15.9 in
15.10 (case Seq.pull (tac st) of
15.11 NONE => raise THM ("rule_by_tactic", 0, [rl])
16.1 --- a/src/Pure/variable.ML Wed Jun 24 20:52:49 2009 +0200
16.2 +++ b/src/Pure/variable.ML Wed Jun 24 21:28:02 2009 +0200
16.3 @@ -51,9 +51,9 @@
16.4 (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
16.5 val importT_terms: term list -> Proof.context -> term list * Proof.context
16.6 val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
16.7 - val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
16.8 + val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
16.9 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
16.10 - val import_thms: bool -> thm list -> Proof.context ->
16.11 + val import: bool -> thm list -> Proof.context ->
16.12 ((ctyp list * cterm list) * thm list) * Proof.context
16.13 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
16.14 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
16.15 @@ -424,7 +424,7 @@
16.16 let val (inst, ctxt') = import_inst is_open ts ctxt
16.17 in (map (TermSubst.instantiate inst) ts, ctxt') end;
16.18
16.19 -fun importT_thms ths ctxt =
16.20 +fun importT ths ctxt =
16.21 let
16.22 val thy = ProofContext.theory_of ctxt;
16.23 val certT = Thm.ctyp_of thy;
16.24 @@ -439,7 +439,7 @@
16.25 val (insts, ctxt') = import_inst is_open ts ctxt;
16.26 in (Proofterm.instantiate insts prf, ctxt') end;
16.27
16.28 -fun import_thms is_open ths ctxt =
16.29 +fun import is_open ths ctxt =
16.30 let
16.31 val thy = ProofContext.theory_of ctxt;
16.32 val cert = Thm.cterm_of thy;
16.33 @@ -457,8 +457,8 @@
16.34 let val ((_, ths'), ctxt') = imp ths ctxt
16.35 in exp ctxt' ctxt (f ctxt' ths') end;
16.36
16.37 -val tradeT = gen_trade importT_thms exportT;
16.38 -val trade = gen_trade (import_thms true) export;
16.39 +val tradeT = gen_trade importT exportT;
16.40 +val trade = gen_trade (import true) export;
16.41
16.42
16.43 (* focus on outermost parameters *)
17.1 --- a/src/Tools/project_rule.ML Wed Jun 24 20:52:49 2009 +0200
17.2 +++ b/src/Tools/project_rule.ML Wed Jun 24 21:28:02 2009 +0200
17.3 @@ -39,7 +39,7 @@
17.4 (case try imp th of
17.5 NONE => (k, th)
17.6 | SOME th' => prems (k + 1) th');
17.7 - val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
17.8 + val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
17.9 fun result i =
17.10 rule
17.11 |> proj i
17.12 @@ -59,7 +59,7 @@
17.13 (case try conj2 th of
17.14 NONE => k
17.15 | SOME th' => projs (k + 1) th');
17.16 - val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
17.17 + val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
17.18 in projects ctxt (1 upto projs 1 rule) raw_rule end;
17.19
17.20 end;