src/Pure/Thy/thy_parse.ML

 val pure_keywords =
  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<",
   "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
 
 val pure_sections =
- [section "oracle" "|> set_oracle" ident,
+ [section "oracle" "|> set_oracle" (name >> strip_quotes),
   section "classes" "|> add_classes" class_decls,
   section "default" "|> add_defsort" sort,
   section "types" "" type_decls,
   section "arities" "|> add_arities" arity_decls,
   section "consts" "|> add_consts" const_decls,