# HG changeset patch
# User wenzelm
# Date 1395157491 -3600
# Node ID 7adec2a527f5315f1dad239bdb83dcc06ae1b9f6
# Parent  ceb8a93460b7abc03a05c3fd48d324b15dd82c38
clarified module arrangement;
more antiquotations;

diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Mar 18 16:16:28 2014 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Mar 18 16:44:51 2014 +0100
@@ -466,9 +466,9 @@
       "(realizes (r) (!!x. PROP P (x))) ==  \
     \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
 
-   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
+   Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false))
      "specify theorems to be expanded during extraction" #>
-   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
+   Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true))
      "specify definitions to be expanded during extraction");
 
 
diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:16:28 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:44:51 2014 +0100
@@ -63,9 +63,9 @@
        ("", idtT --> paramsT, Delimfix "_"),
        ("", paramT --> paramsT, Delimfix "_")]
   |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
-      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3)),
-       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
-       (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
+       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+       (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
   |> Sign.add_trrules (map Syntax.Parse_Print_Rule
       [(Ast.mk_appl (Ast.Constant "_Lam")
           [Ast.mk_appl (Ast.Constant "_Lam0")
diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 18 16:44:51 2014 +0100
@@ -211,12 +211,6 @@
 use "Syntax/syntax_phases.ML";
 use "Isar/local_defs.ML";
 
-(*proof term operations*)
-use "Proof/reconstruct.ML";
-use "Proof/proof_syntax.ML";
-use "Proof/proof_rewrite_rules.ML";
-use "Proof/proof_checker.ML";
-
 (*outer syntax*)
 use "Isar/token.ML";
 use "Isar/keyword.ML";
@@ -271,6 +265,13 @@
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
+(*proof term operations*)
+use "Proof/reconstruct.ML";
+use "Proof/proof_syntax.ML";
+use "Proof/proof_rewrite_rules.ML";
+use "Proof/proof_checker.ML";
+use "Proof/extraction.ML";
+
 (*theory documents*)
 use "System/isabelle_system.ML";
 use "Thy/term_style.ML";
@@ -290,8 +291,6 @@
 
 use "subgoal.ML";
 
-use "Proof/extraction.ML";
-
 
 (* Isabelle/Isar system *)