clarified context;
authorwenzelm
Tue Jul 28 23:14:40 2015 +0200 (2015-07-28)
changeset 60826695cf1fab6cc
parent 60825 bacfb7c45d81
child 60827 31e08fe243f1
clarified context;
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 21:47:03 2015 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 23:14:40 2015 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4              | _ => AbsP ("H", SOME p, prf)))
     1.5            (rec_fns ~~ Thm.prems_of thm)
     1.6            (Proofterm.proof_combP
     1.7 -            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
     1.8 +            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
     1.9  
    1.10      val r' =
    1.11        if null is then r
    1.12 @@ -212,10 +212,10 @@
    1.13                (AbsP ("H", SOME (Logic.varify_global p), prf)))
    1.14            (prems ~~ rs)
    1.15            (Proofterm.proof_combP
    1.16 -            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
    1.17 +            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
    1.18      val prf' =
    1.19        Extraction.abs_corr_shyps thy' exhaust []
    1.20 -        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
    1.21 +        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
    1.22      val r' =
    1.23        Logic.varify_global (Abs ("y", T,
    1.24          (fold_rev (Term.abs o dest_Free) rs
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 21:47:03 2015 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 23:14:40 2015 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4    | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
     2.5  
     2.6  fun prf_of thy thm =
     2.7 -  Reconstruct.proof_of thm
     2.8 +  Reconstruct.proof_of thy thm
     2.9    |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
    2.10  
    2.11  fun subsets [] = [[]]
     3.1 --- a/src/Pure/Proof/extraction.ML	Tue Jul 28 21:47:03 2015 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jul 28 23:14:40 2015 +0200
     3.3 @@ -769,9 +769,9 @@
     3.4  
     3.5        | extr d vs ts Ts hs _ defs = error "extr: bad proof";
     3.6  
     3.7 -    fun prep_thm vs thm =
     3.8 +    fun prep_thm vs raw_thm =
     3.9        let
    3.10 -        val thy = Thm.theory_of_thm thm;
    3.11 +        val thm = Thm.transfer thy raw_thm;
    3.12          val prop = Thm.prop_of thm;
    3.13          val prf = Thm.proof_of thm;
    3.14          val name = Thm.derivation_name thm;
     4.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 21:47:03 2015 +0200
     4.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 23:14:40 2015 +0200
     4.3 @@ -14,7 +14,7 @@
     4.4    val read_term: theory -> bool -> typ -> string -> term
     4.5    val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
     4.6    val proof_syntax: Proofterm.proof -> theory -> theory
     4.7 -  val proof_of: bool -> thm -> Proofterm.proof
     4.8 +  val proof_of: theory -> bool -> thm -> Proofterm.proof
     4.9    val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    4.10    val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
    4.11  end;
    4.12 @@ -235,9 +235,9 @@
    4.13        (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
    4.14    end;
    4.15  
    4.16 -fun proof_of full thm =
    4.17 +fun proof_of thy full raw_thm =
    4.18    let
    4.19 -    val thy = Thm.theory_of_thm thm;
    4.20 +    val thm = Thm.transfer thy raw_thm;
    4.21      val prop = Thm.full_prop_of thm;
    4.22      val prf = Thm.proof_of thm;
    4.23      val prf' =
    4.24 @@ -253,6 +253,6 @@
    4.25      (term_of_proof prf);
    4.26  
    4.27  fun pretty_proof_of ctxt full th =
    4.28 -  pretty_proof ctxt (proof_of full th);
    4.29 +  pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
    4.30  
    4.31  end;
     5.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Jul 28 21:47:03 2015 +0200
     5.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 28 23:14:40 2015 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4    val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
     5.5    val prop_of' : term list -> Proofterm.proof -> term
     5.6    val prop_of : Proofterm.proof -> term
     5.7 -  val proof_of : thm -> Proofterm.proof
     5.8 +  val proof_of : theory -> thm -> Proofterm.proof
     5.9    val expand_proof : theory -> (string * term option) list ->
    5.10      Proofterm.proof -> Proofterm.proof
    5.11  end;
    5.12 @@ -324,8 +324,9 @@
    5.13  val prop_of' = Envir.beta_eta_contract oo prop_of0;
    5.14  val prop_of = prop_of' [];
    5.15  
    5.16 -fun proof_of thm =
    5.17 -  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    5.18 +fun proof_of thy raw_thm =
    5.19 +  let val thm = Thm.transfer thy raw_thm
    5.20 +  in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end;
    5.21  
    5.22  
    5.23