Variable.import(T): result includes fixed types/terms;
authorwenzelm
Wed Jul 26 19:37:41 2006 +0200 (2006-07-26)
changeset 20218be3bfb0699ba
parent 20217 25b068a99d2b
child 20219 3bff4719f3d6
Variable.import(T): result includes fixed types/terms;
doc-src/IsarImplementation/Thy/proof.thy
src/HOL/Tools/datatype_package.ML
src/Provers/project_rule.ML
src/Pure/Isar/element.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/Tools/invoke.ML
src/Pure/tactic.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Wed Jul 26 19:23:04 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Wed Jul 26 19:37:41 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
     1.6    @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
     1.7 -  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
     1.8 +  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\
     1.9    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
    1.10    @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
    1.11    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Jul 26 19:23:04 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Jul 26 19:37:41 2006 +0200
     2.3 @@ -810,7 +810,7 @@
     2.4        ||>> apply_theorems [raw_induction];
     2.5      val sign = Theory.sign_of thy1;
     2.6  
     2.7 -    val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction);
     2.8 +    val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
     2.9  
    2.10      fun err t = error ("Ill-formed predicate in induction rule: " ^
    2.11        Sign.string_of_term sign t);
     3.1 --- a/src/Provers/project_rule.ML	Wed Jul 26 19:23:04 2006 +0200
     3.2 +++ b/src/Provers/project_rule.ML	Wed Jul 26 19:37:41 2006 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4        (case try imp th of
     3.5          NONE => (k, th)
     3.6        | SOME th' => prems (k + 1) th');
     3.7 -    val ([rule], ctxt') = Variable.import true [raw_rule] ctxt;
     3.8 +    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     3.9      fun result i =
    3.10        rule
    3.11        |> proj i
    3.12 @@ -57,7 +57,7 @@
    3.13        (case try conj2 th of
    3.14          NONE => k
    3.15        | SOME th' => projs (k + 1) th');
    3.16 -    val ([rule], _) = Variable.import true [raw_rule] ctxt;
    3.17 +    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
    3.18    in projects ctxt (1 upto projs 1 rule) raw_rule end;
    3.19  
    3.20  end;
     4.1 --- a/src/Pure/Isar/element.ML	Wed Jul 26 19:23:04 2006 +0200
     4.2 +++ b/src/Pure/Isar/element.ML	Wed Jul 26 19:37:41 2006 +0200
     4.3 @@ -219,7 +219,7 @@
     4.4      val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     4.5      val As = Logic.strip_imp_prems (Thm.term_of prop');
     4.6      fun var (x, T) = (ProofContext.revert_skolem ctxt' x, SOME T);
     4.7 -  in (("", (map var xs, As)), ctxt') end;
     4.8 +  in (("", (map (var o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
     4.9  
    4.10  in
    4.11  
    4.12 @@ -231,7 +231,7 @@
    4.13      val th = Goal.norm_hhf raw_th;
    4.14      val is_elim = ObjectLogic.is_elim th;
    4.15  
    4.16 -    val ([th'], ctxt') = Variable.import true [th] ctxt;
    4.17 +    val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
    4.18      val prop = Thm.prop_of th';
    4.19      val (prems, concl) = Logic.strip_horn prop;
    4.20      val concl_term = ObjectLogic.drop_judgment thy concl;
     5.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 26 19:23:04 2006 +0200
     5.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 26 19:37:41 2006 +0200
     5.3 @@ -209,7 +209,7 @@
     5.4      val instT =
     5.5        fold (Term.add_tvarsT o #2) params []
     5.6        |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
     5.7 -    val (rule' :: terms', ctxt') =
     5.8 +    val ((_, rule' :: terms'), ctxt') =
     5.9        Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
    5.10  
    5.11      val vars' =
     6.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Jul 26 19:23:04 2006 +0200
     6.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Jul 26 19:37:41 2006 +0200
     6.3 @@ -329,7 +329,7 @@
     6.4    | mutual_rule _ [th] = SOME ([0], th)
     6.5    | mutual_rule ctxt (ths as th :: _) =
     6.6        let
     6.7 -        val (ths', ctxt') = Variable.import true ths ctxt;
     6.8 +        val ((_, ths'), ctxt') = Variable.import true ths ctxt;
     6.9          val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
    6.10          val (ns, rls) = split_list (map #2 rules);
    6.11        in
     7.1 --- a/src/Pure/Tools/codegen_theorems.ML	Wed Jul 26 19:23:04 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jul 26 19:37:41 2006 +0200
     7.3 @@ -581,7 +581,7 @@
     7.4      fun cmp_thms (thm1, thm2) =
     7.5        not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
     7.6      fun unvarify thms =
     7.7 -      #1 (Variable.import true thms (ProofContext.init thy));
     7.8 +      #2 (#1 (Variable.import true thms (ProofContext.init thy)));
     7.9      val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
    7.10    in
    7.11      thms
     8.1 --- a/src/Pure/Tools/invoke.ML	Wed Jul 26 19:23:04 2006 +0200
     8.2 +++ b/src/Pure/Tools/invoke.ML	Wed Jul 26 19:37:41 2006 +0200
     8.3 @@ -63,7 +63,7 @@
     8.4        Seq.map (Proof.map_context (fn ctxt =>
     8.5          let
     8.6            val ([res_types, res_params, res_prems], ctxt'') =
     8.7 -            fold_burrow (Variable.import false) results ctxt';
     8.8 +            fold_burrow (apfst snd oo Variable.import false) results ctxt';
     8.9  
    8.10            val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
    8.11            val params'' = map (Thm.term_of o Drule.dest_term) res_params;
     9.1 --- a/src/Pure/tactic.ML	Wed Jul 26 19:23:04 2006 +0200
     9.2 +++ b/src/Pure/tactic.ML	Wed Jul 26 19:37:41 2006 +0200
     9.3 @@ -136,7 +136,7 @@
     9.4  fun rule_by_tactic tac rl =
     9.5    let
     9.6      val ctxt = Variable.thm_context rl;
     9.7 -    val ([st], ctxt') = Variable.import true [rl] ctxt;
     9.8 +    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
     9.9    in
    9.10      (case Seq.pull (tac st) of
    9.11        NONE => raise THM ("rule_by_tactic", 0, [rl])