src/Pure/Thy/thy_parse.ML
changeset 3770 294b5905f4eb
parent 3764 fe7719aee219
child 3780 ac23a9ab3cd6
equal deleted inserted replaced
3769:931c336b0707 3770:294b5905f4eb
   531 val pure_keywords =
   531 val pure_keywords =
   532  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
   532  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
   533   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
   533   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
   534 
   534 
   535 val pure_sections =
   535 val pure_sections =
   536  [section "oracle" "|> set_oracle" (name >> strip_quotes),
   536  [section "oracle" "|> Theory.set_oracle" (name >> strip_quotes),
   537   section "classes" "|> Theory.add_classes" class_decls,
   537   section "classes" "|> Theory.add_classes" class_decls,
   538   section "default" "|> Theory.add_defsort" sort,
   538   section "default" "|> Theory.add_defsort" sort,
   539   section "types" "" type_decls,
   539   section "types" "" type_decls,
   540   section "arities" "|> Theory.add_arities" arity_decls,
   540   section "arities" "|> Theory.add_arities" arity_decls,
   541   section "consts" "|> Theory.add_consts" const_decls,
   541   section "consts" "|> Theory.add_consts" const_decls,