# HG changeset patch # User wenzelm # Date 1245871682 -7200 # Node ID 71af1fd6a5e4422b23ebe5b981cf29b68e424868 # Parent 7c10b13d49fea535df193fcfe02126ca143f5e2f renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again); diff -r 7c10b13d49fe -r 71af1fd6a5e4 doc-src/IsarImplementation/Thy/Proof.thy --- 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 diff -r 7c10b13d49fe -r 71af1fd6a5e4 doc-src/IsarImplementation/Thy/document/Proof.tex --- 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}). diff -r 7c10b13d49fe -r 71af1fd6a5e4 doc-src/more_antiquote.ML --- 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 = diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/HOL/Library/reflection.ML --- 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 diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/HOL/Tools/Datatype/datatype.ML --- 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); diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/HOL/Tools/res_axioms.ML --- 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; diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/HOL/Tools/transfer_data.ML --- 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) diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/attrib.ML --- 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 = diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/class.ML --- 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; diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/element.ML --- 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; diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/local_defs.ML --- 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 diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/obtain.ML --- 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); diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/rule_cases.ML --- 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 diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/subgoal.ML --- 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; diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/tactic.ML --- 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]) diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/variable.ML --- 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 *) diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Tools/project_rule.ML --- 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;