# HG changeset patch
# User wenzelm
# Date 1282924780 -7200
# Node ID 89ae862057399c2d1264b249c078e64f74dde6c4
# Parent  378ffc903bedc51263e9dbfcf83a3e2fb2faba06
more antiquotations;

diff -r 378ffc903bed -r 89ae86205739 src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -371,7 +371,7 @@
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
 val (_, export_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
+  (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
diff -r 378ffc903bed -r 89ae86205739 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -175,7 +175,7 @@
    "equivariance theorem declaration" #>
   Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
     "equivariance theorem declaration (without checking the form of the lemma)" #>
-  PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get);
+  PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
 
 
 end;
diff -r 378ffc903bed -r 89ae86205739 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/String.thy	Fri Aug 27 17:59:40 2010 +0200
@@ -53,7 +53,7 @@
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;
 in
-  PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+  PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
 end
 *}
diff -r 378ffc903bed -r 89ae86205739 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -679,9 +679,11 @@
 
 end;
 
-val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
-  (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
-    (t, procedure t)))));
+val (_, oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (@{binding cooper},
+    (fn (ctxt, t) =>
+      (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
+        (t, procedure t)))));
 
 val comp_ss = HOL_ss addsimps @{thms semiring_norm};
 
diff -r 378ffc903bed -r 89ae86205739 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -310,18 +310,18 @@
 (* setup *)
 
 val setup =
-  Attrib.setup (Binding.name "smt_solver")
+  Attrib.setup @{binding smt_solver}
     (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
   setup_timeout #>
   setup_trace #>
   setup_fixed_certificates #>
-  Attrib.setup (Binding.name "smt_certificates")
+  Attrib.setup @{binding smt_certificates}
     (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates" #>
-  Method.setup (Binding.name "smt") smt_method
+  Method.setup @{binding smt} smt_method
     "Applies an SMT solver to the current goal."