--- 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");
--- 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")
--- 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 *)