# HG changeset patch # User wenzelm # Date 1153935461 -7200 # Node ID be3bfb0699ba247abcbbfa8e73375bd0e8d2538b # Parent 25b068a99d2b22319c1962c8946ab5c35523b9eb Variable.import(T): result includes fixed types/terms; diff -r 25b068a99d2b -r be3bfb0699ba doc-src/IsarImplementation/Thy/proof.thy --- 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"} \\ diff -r 25b068a99d2b -r be3bfb0699ba src/HOL/Tools/datatype_package.ML --- 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); diff -r 25b068a99d2b -r be3bfb0699ba src/Provers/project_rule.ML --- 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; diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Isar/element.ML --- 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; diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Isar/obtain.ML --- 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' = diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Isar/rule_cases.ML --- 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 diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Tools/codegen_theorems.ML --- 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 diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Tools/invoke.ML --- 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; diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/tactic.ML --- 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])