src/Pure/Isar/obtain.ML

   (case Thm.prems_of th of
     [prem] =>
       if Thm.concl_of th aconv thesis andalso
         Logic.strip_assums_concl prem aconv thesis then th
       else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
-  | [] => error "Goal solved -- nothing guessed."
+  | [] => error "Goal solved -- nothing guessed"
   | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
 
 fun result tac facts ctxt =
   let
     val thy = ProofContext.theory_of ctxt;