prefer user-space tool within Pure.thy;
authorwenzelm
Sun Feb 16 17:25:03 2014 +0100 (2014-02-16)
changeset 55516d0157612ebe5
parent 55515 0e161deca64d
child 55517 a3870c12f254
prefer user-space tool within Pure.thy;
src/Pure/ML/ml_thms.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_thms.ML	Sun Feb 16 17:17:26 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_thms.ML	Sun Feb 16 17:25:03 2014 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  (* attribute source *)
     1.5  
     1.6  val _ = Theory.setup
     1.7 -  (ML_Context.add_antiq (Binding.name "attributes")
     1.8 +  (ML_Context.add_antiq @{binding attributes}
     1.9      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
    1.10        let
    1.11          val ctxt = Context.the_proof context;
    1.12 @@ -73,10 +73,10 @@
    1.13    in (Context.Proof ctxt'', decl) end;
    1.14  
    1.15  val _ = Theory.setup
    1.16 -  (ML_Context.add_antiq (Binding.name "thm")
    1.17 +  (ML_Context.add_antiq @{binding thm}
    1.18      (Scan.depend (fn context =>
    1.19        Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
    1.20 -   ML_Context.add_antiq (Binding.name "thms")
    1.21 +   ML_Context.add_antiq @{binding thms}
    1.22      (Scan.depend (fn context =>
    1.23        Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
    1.24  
    1.25 @@ -89,7 +89,7 @@
    1.26  val goals1 = Scan.repeat1 goal;
    1.27  
    1.28  val _ = Theory.setup
    1.29 -  (ML_Context.add_antiq (Binding.name "lemma")
    1.30 +  (ML_Context.add_antiq @{binding lemma}
    1.31      (Scan.depend (fn context =>
    1.32        Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) --
    1.33        (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >>
     2.1 --- a/src/Pure/Pure.thy	Sun Feb 16 17:17:26 2014 +0100
     2.2 +++ b/src/Pure/Pure.thy	Sun Feb 16 17:25:03 2014 +0100
     2.3 @@ -101,6 +101,7 @@
     2.4      "ProofGeneral.inform_file_retracted" :: control
     2.5  begin
     2.6  
     2.7 +ML_file "ML/ml_thms.ML"
     2.8  ML_file "Isar/isar_syn.ML"
     2.9  ML_file "Isar/calculation.ML"
    2.10  ML_file "Tools/rail.ML"
     3.1 --- a/src/Pure/ROOT	Sun Feb 16 17:17:26 2014 +0100
     3.2 +++ b/src/Pure/ROOT	Sun Feb 16 17:25:03 2014 +0100
     3.3 @@ -151,7 +151,6 @@
     3.4      "ML/ml_statistics_dummy.ML"
     3.5      "ML/ml_statistics_polyml-5.5.0.ML"
     3.6      "ML/ml_syntax.ML"
     3.7 -    "ML/ml_thms.ML"
     3.8      "PIDE/active.ML"
     3.9      "PIDE/command.ML"
    3.10      "PIDE/document.ML"
     4.1 --- a/src/Pure/ROOT.ML	Sun Feb 16 17:17:26 2014 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Sun Feb 16 17:25:03 2014 +0100
     4.3 @@ -260,7 +260,6 @@
     4.4  use "Isar/spec_rules.ML";
     4.5  use "Isar/specification.ML";
     4.6  use "Isar/typedecl.ML";
     4.7 -use "ML/ml_thms.ML";
     4.8  
     4.9  (*toplevel transactions*)
    4.10  use "Isar/proof_node.ML";