src/Pure/Isar/specification.ML
changeset 21860 c4492c6bf450
parent 21793 74409847e349
child 22744 5cbe966d67a2
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:14 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:15 2006 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4  fun gen_theorem prep_att prep_stmt
     1.5      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
     1.6    let
     1.7 -    val _ = LocalTheory.assert lthy0;
     1.8 +    val _ = LocalTheory.affirm lthy0;
     1.9      val thy = ProofContext.theory_of lthy0;
    1.10  
    1.11      val (loc, ctxt, lthy) =