src/HOL/Library/rewrite.ML

       in ((pats', ths, (to', ctxt)), ctxt'') end
 
     val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
 
     val subst_parser =
-      let val scan = raw_pattern -- to_parser -- Parse.xthms1
+      let val scan = raw_pattern -- to_parser -- Parse.thms1
       in context_lift scan prep_args end
   in
     Method.setup @{binding rewrite} (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
         SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))