Attrib.eval_thms;
authorwenzelm
Wed Sep 26 19:18:00 2007 +0200 (2007-09-26)
changeset 2472504b676d1a1fe
parent 24724 0df74bb87a13
child 24726 fcf13a91cda2
Attrib.eval_thms;
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Sep 26 19:17:59 2007 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Sep 26 19:18:00 2007 +0200
     1.3 @@ -388,20 +388,18 @@
     1.4  
     1.5  fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
     1.6    let
     1.7 +    val ctxt = ProofContext.init thy;
     1.8      val read_i = Sign.simple_read_term thy Ind_Syntax.iT;
     1.9      val rec_tms = map read_i srec_tms;
    1.10      val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
    1.11      val dom_sum =
    1.12        if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
    1.13        else read_i sdom;
    1.14 -  in
    1.15 -    thy
    1.16 -    |> IsarCmd.apply_theorems raw_monos
    1.17 -    ||>> IsarCmd.apply_theorems raw_type_intrs
    1.18 -    ||>> IsarCmd.apply_theorems raw_type_elims
    1.19 -    |-> (fn ((monos, type_intrs), type_elims) =>
    1.20 -          add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
    1.21 -  end;
    1.22 +    val monos = Attrib.eval_thms ctxt raw_monos;
    1.23 +    val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
    1.24 +    val type_elims = Attrib.eval_thms ctxt raw_type_elims;
    1.25 +  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
    1.26 +
    1.27  
    1.28  (* outer syntax *)
    1.29  
     2.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Sep 26 19:17:59 2007 +0200
     2.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Sep 26 19:18:00 2007 +0200
     2.3 @@ -165,14 +165,13 @@
     2.4    end;
     2.5  
     2.6  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
     2.7 -  thy
     2.8 -  |> IsarCmd.apply_theorems [raw_elim]
     2.9 -  ||>> IsarCmd.apply_theorems [raw_induct]
    2.10 -  ||>> IsarCmd.apply_theorems raw_case_eqns
    2.11 -  ||>> IsarCmd.apply_theorems raw_recursor_eqns
    2.12 -  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
    2.13 -          rep_datatype_i (PureThy.single_thm "elimination" elims)
    2.14 -            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
    2.15 +  let
    2.16 +    val ctxt = ProofContext.init thy;
    2.17 +    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
    2.18 +    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
    2.19 +    val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
    2.20 +    val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
    2.21 +  in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
    2.22  
    2.23  
    2.24  (* theory setup *)