1.1 --- a/etc/isar-keywords-ZF.el	Sat Mar 29 19:14:03 2008 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4      "Isabelle\\.command"
     1.5      "ML"
     1.6      "ML_command"
     1.7 -    "ML_setup"
     1.8      "ML_val"
     1.9      "ProofGeneral\\.inform_file_processed"
    1.10      "ProofGeneral\\.inform_file_retracted"
    1.11 @@ -266,8 +265,7 @@
    1.12      "undos_proof"))
    1.13  
    1.14  (defconst isar-keywords-diag
    1.15 -  '("ML"
    1.16 -    "ML_command"
    1.17 +  '("ML_command"
    1.18      "ML_val"
    1.19      "cd"
    1.20      "class_deps"
    1.21 @@ -321,7 +319,6 @@
    1.22      "touch_thy"
    1.23      "typ"
    1.24      "unused_thms"
    1.25 -    "use"
    1.26      "use_thy"
    1.27      "value"
    1.28      "welcome"))
    1.29 @@ -342,7 +339,7 @@
    1.30      "subsubsection"))
    1.31  
    1.32  (defconst isar-keywords-theory-decl
    1.33 -  '("ML_setup"
    1.34 +  '("ML"
    1.35      "abbreviation"
    1.36      "arities"
    1.37      "axclass"
    1.38 @@ -405,7 +402,8 @@
    1.39      "typed_print_translation"
    1.40      "typedecl"
    1.41      "types"
    1.42 -    "types_code"))
    1.43 +    "types_code"
    1.44 +    "use"))
    1.45  
    1.46  (defconst isar-keywords-theory-script
    1.47    '("inductive_cases"))

     2.1 --- a/etc/isar-keywords.el	Sat Mar 29 19:14:03 2008 +0100
     2.2 +++ b/etc/isar-keywords.el	Sat Mar 29 19:14:03 2008 +0100
     2.3 @@ -12,7 +12,6 @@
     2.4      "Isabelle\\.command"
     2.5      "ML"
     2.6      "ML_command"
     2.7 -    "ML_setup"
     2.8      "ML_val"
     2.9      "ProofGeneral\\.inform_file_processed"
    2.10      "ProofGeneral\\.inform_file_retracted"
    2.11 @@ -326,8 +325,7 @@
    2.12      "undos_proof"))
    2.13  
    2.14  (defconst isar-keywords-diag
    2.15 -  '("ML"
    2.16 -    "ML_command"
    2.17 +  '("ML_command"
    2.18      "ML_val"
    2.19      "cd"
    2.20      "class_deps"
    2.21 @@ -389,7 +387,6 @@
    2.22      "touch_thy"
    2.23      "typ"
    2.24      "unused_thms"
    2.25 -    "use"
    2.26      "use_thy"
    2.27      "value"
    2.28      "welcome"))
    2.29 @@ -410,7 +407,7 @@
    2.30      "subsubsection"))
    2.31  
    2.32  (defconst isar-keywords-theory-decl
    2.33 -  '("ML_setup"
    2.34 +  '("ML"
    2.35      "abbreviation"
    2.36      "arities"
    2.37      "atom_decl"
    2.38 @@ -497,7 +494,8 @@
    2.39      "typed_print_translation"
    2.40      "typedecl"
    2.41      "types"
    2.42 -    "types_code"))
    2.43 +    "types_code"
    2.44 +    "use"))
    2.45  
    2.46  (defconst isar-keywords-theory-script
    2.47    '("inductive_cases"))

     3.1 --- a/lib/jedit/isabelle.xml	Sat Mar 29 19:14:03 2008 +0100
     3.2 +++ b/lib/jedit/isabelle.xml	Sat Mar 29 19:14:03 2008 +0100
     3.3 @@ -36,9 +36,8 @@
     3.4        <OPERATOR>.</OPERATOR>
     3.5        <OPERATOR>..</OPERATOR>
     3.6        <INVALID>Isabelle.command</INVALID>
     3.7 -      <LABEL>ML</LABEL>
     3.8 +      <OPERATOR>ML</OPERATOR>
     3.9        <LABEL>ML_command</LABEL>
    3.10 -      <OPERATOR>ML_setup</OPERATOR>
    3.11        <LABEL>ML_val</LABEL>
    3.12        <OPERATOR>abbreviation</OPERATOR>
    3.13        <KEYWORD4>actions</KEYWORD4>
    3.14 @@ -325,7 +324,7 @@
    3.15        <INVALID>undos_proof</INVALID>
    3.16        <OPERATOR>unfolding</OPERATOR>
    3.17        <LABEL>unused_thms</LABEL>
    3.18 -      <LABEL>use</LABEL>
    3.19 +      <OPERATOR>use</OPERATOR>
    3.20        <LABEL>use_thy</LABEL>
    3.21        <KEYWORD4>uses</KEYWORD4>
    3.22        <OPERATOR>using</OPERATOR>