src/ZF/Tools/induct_tacs.ML
changeset 26336 a0e2b706ce73
parent 24867 e5b55d7be9bb
child 26618 f3535afb58e8
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4    val induct_tac: string -> int -> tactic
     1.5    val exhaust_tac: string -> int -> tactic
     1.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
     1.7 -  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
     1.8 -    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
     1.9 +  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
    1.10 +    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
    1.11    val setup: theory -> theory
    1.12  end;
    1.13  
    1.14 @@ -167,8 +167,8 @@
    1.15  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
    1.16    let
    1.17      val ctxt = ProofContext.init thy;
    1.18 -    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
    1.19 -    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
    1.20 +    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
    1.21 +    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
    1.22      val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
    1.23      val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
    1.24    in rep_datatype_i elim induct case_eqns recursor_eqns thy end;