src/ZF/Tools/induct_tacs.ML
changeset 55740 11dd48f84441
parent 46961 5c6955f487e5
child 56231 b98813774a63
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 10:50:12 2014 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 11:36:04 2014 +0100
     1.3 @@ -166,8 +166,8 @@
     1.4  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy;
     1.7 -    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
     1.8 -    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
     1.9 +    val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
    1.10 +    val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
    1.11      val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
    1.12      val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
    1.13    in rep_datatype_i elim induct case_eqns recursor_eqns thy end;