--- 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
--- 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;
--- 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
*}
--- 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};
--- 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."