src/HOL/Tools/BNF/bnf_lift.ML

 
 val parse_plugins =
   Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
     (K Plugin_Name.default_filter) >> Plugins_Option >> single;
 
-val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.xthm);
+val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
 
 in
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf}