# HG changeset patch
# User wenzelm
# Date 1392567903 -3600
# Node ID d0157612ebe588bbeab8c94d817c45b3e5b6f673
# Parent  0e161deca64db3890980cedb2d4b5f47773dd557
prefer user-space tool within Pure.thy;

diff -r 0e161deca64d -r d0157612ebe5 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Feb 16 17:17:26 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sun Feb 16 17:25:03 2014 +0100
@@ -35,7 +35,7 @@
 (* attribute source *)
 
 val _ = Theory.setup
-  (ML_Context.add_antiq (Binding.name "attributes")
+  (ML_Context.add_antiq @{binding attributes}
     (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
       let
         val ctxt = Context.the_proof context;
@@ -73,10 +73,10 @@
   in (Context.Proof ctxt'', decl) end;
 
 val _ = Theory.setup
-  (ML_Context.add_antiq (Binding.name "thm")
+  (ML_Context.add_antiq @{binding thm}
     (Scan.depend (fn context =>
       Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
-   ML_Context.add_antiq (Binding.name "thms")
+   ML_Context.add_antiq @{binding thms}
     (Scan.depend (fn context =>
       Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
 
@@ -89,7 +89,7 @@
 val goals1 = Scan.repeat1 goal;
 
 val _ = Theory.setup
-  (ML_Context.add_antiq (Binding.name "lemma")
+  (ML_Context.add_antiq @{binding lemma}
     (Scan.depend (fn context =>
       Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) --
       (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >>
diff -r 0e161deca64d -r d0157612ebe5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Feb 16 17:17:26 2014 +0100
+++ b/src/Pure/Pure.thy	Sun Feb 16 17:25:03 2014 +0100
@@ -101,6 +101,7 @@
     "ProofGeneral.inform_file_retracted" :: control
 begin
 
+ML_file "ML/ml_thms.ML"
 ML_file "Isar/isar_syn.ML"
 ML_file "Isar/calculation.ML"
 ML_file "Tools/rail.ML"
diff -r 0e161deca64d -r d0157612ebe5 src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Feb 16 17:17:26 2014 +0100
+++ b/src/Pure/ROOT	Sun Feb 16 17:25:03 2014 +0100
@@ -151,7 +151,6 @@
     "ML/ml_statistics_dummy.ML"
     "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
-    "ML/ml_thms.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/document.ML"
diff -r 0e161deca64d -r d0157612ebe5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Feb 16 17:17:26 2014 +0100
+++ b/src/Pure/ROOT.ML	Sun Feb 16 17:25:03 2014 +0100
@@ -260,7 +260,6 @@
 use "Isar/spec_rules.ML";
 use "Isar/specification.ML";
 use "Isar/typedecl.ML";
-use "ML/ml_thms.ML";
 
 (*toplevel transactions*)
 use "Isar/proof_node.ML";