src/Pure/Isar/isar_thy.ML
changeset 6890 05732285677e
parent 6888 d0c68ebdabc5
child 6904 4125d6b6d8f9
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Sat Jul 03 00:21:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sat Jul 03 00:22:53 1999 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5  (* formal comments *)
     1.6  
     1.7 -fun add_txt comment prf = prf;
     1.8 +fun add_txt comment = ProofHistory.apply Proof.assert_forward;
     1.9  fun add_text comment thy = thy;
    1.10  fun add_title title author date thy = thy;
    1.11  val add_chapter = add_text;