src/Pure/thm.ML

--- a/src/Pure/thm.ML	Tue Jul 30 15:09:25 2013 +0200
+++ b/src/Pure/thm.ML	Tue Jul 30 15:20:38 2013 +0200
@@ -978,7 +978,7 @@
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = B})
         else err "not equal"
-     | _ =>  err"major premise")
+     | _ =>  err "major premise")
   end;