# HG changeset patch
# User wenzelm
# Date 1309526163 -7200
# Node ID 3803869014aa8b90a6a43098beea3f0b032dc41f
# Parent  1c43134ff98806dd89cf8f0faa0739d87cf984ba
proper @{binding} antiquotations (relevant for formal references);

diff -r 1c43134ff988 -r 3803869014aa src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -1902,7 +1902,7 @@
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val ([dots], ctxt') =
-      Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix ("...", [], 1000))] ctxt 
+      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt 
     (* check expected values *)
     val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
     val () =
diff -r 1c43134ff988 -r 3803869014aa src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -408,8 +408,10 @@
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
         val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
-        val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
-          ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
+        (* FIXME proper naming convention for local_theory *)
+        val ((prop_def, _), ctxt') =
+          Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
+            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
         val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
         val (counterexample, result) = dynamic_value_strict (true, opts)
           (Existential_Counterexample.get, Existential_Counterexample.put,
diff -r 1c43134ff988 -r 3803869014aa src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -884,7 +884,7 @@
         val (_, thy') = Inductive.add_inductive_global
           {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
            no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
-          [((Binding.name "quickcheckp", T), NoSyn)] []
+          [((@{binding quickcheckp}, T), NoSyn)] []
           [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
         val pred = HOLogic.mk_Trueprop (list_comb
           (Const (Sign.intern_const thy' "quickcheckp", T),
diff -r 1c43134ff988 -r 3803869014aa src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -163,7 +163,7 @@
   end;
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "holds_by_evaluation",
+  (Thm.add_oracle (@{binding holds_by_evaluation},
   fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
 
 fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
@@ -338,7 +338,7 @@
 
 val _ =
   Context.>> (Context.map_theory
-    (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
+    (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
 
 local
 
diff -r 1c43134ff988 -r 3803869014aa src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -58,9 +58,10 @@
 
 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
 
-val setup = Method.setup (Binding.name "code_simp")
-  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
-  "simplification with code equations"
+val setup =
+  Method.setup @{binding code_simp}
+    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
+    "simplification with code equations"
   #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
 
 
diff -r 1c43134ff988 -r 3803869014aa src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/Tools/nbe.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -78,7 +78,7 @@
 val get_triv_classes = map fst o Triv_Class_Data.get;
 
 val (_, triv_of_class) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
+  (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
     Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
 
 in
@@ -589,7 +589,7 @@
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "normalization_by_evaluation",
+  (Thm.add_oracle (@{binding normalization_by_evaluation},
     fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
       mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
 
diff -r 1c43134ff988 -r 3803869014aa src/Tools/value.ML
--- a/src/Tools/value.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/Tools/value.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -69,7 +69,7 @@
           (value_cmd some_name modes t)));
 
 val antiq_setup =
-  Thy_Output.antiquotation (Binding.name "value")
+  Thy_Output.antiquotation @{binding value}
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source