# HG changeset patch # User wenzelm # Date 1368643165 -7200 # Node ID e91359bfc84abcf9dbb36b427b3668e3a7e28bcd # Parent 3b18ef9df768d6ff2500649c42adec66e6312f7c tuned; diff -r 3b18ef9df768 -r e91359bfc84a src/Pure/ROOT --- a/src/Pure/ROOT Wed May 15 20:34:42 2013 +0200 +++ b/src/Pure/ROOT Wed May 15 20:39:25 2013 +0200 @@ -134,14 +134,14 @@ "Isar/token.ML" "Isar/toplevel.ML" "Isar/typedecl.ML" + "ML/exn_properties_dummy.ML" + "ML/exn_properties_polyml.ML" "ML/install_pp_polyml.ML" "ML/ml_antiquote.ML" "ML/ml_compiler.ML" "ML/ml_compiler_polyml.ML" "ML/ml_context.ML" "ML/ml_env.ML" - "ML/exn_properties_dummy.ML" - "ML/exn_properties_polyml.ML" "ML/ml_lex.ML" "ML/ml_parse.ML" "ML/ml_statistics_dummy.ML" @@ -193,8 +193,8 @@ "Thy/thy_output.ML" "Thy/thy_syntax.ML" "Tools/build.ML" + "Tools/legacy_xml_syntax.ML" "Tools/named_thms.ML" - "Tools/legacy_xml_syntax.ML" "Tools/proof_general.ML" "assumption.ML" "axclass.ML"