more antiquotations;
authorwenzelm
Fri Aug 27 17:59:40 2010 +0200 (2010-08-27)
changeset 3880889ae86205739
parent 38807 378ffc903bed
child 38830 51efa72555bb
more antiquotations;
src/HOL/Matrix/Compute_Oracle/compute.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/String.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:23:57 2010 +0200
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:59:40 2010 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
     1.5  
     1.6  val (_, export_oracle) = Context.>>> (Context.map_theory_result
     1.7 -  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
     1.8 +  (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
     1.9      let
    1.10          val shyptab = add_shyps shyps Sorttab.empty
    1.11          fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
     2.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:23:57 2010 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:59:40 2010 +0200
     2.3 @@ -175,7 +175,7 @@
     2.4     "equivariance theorem declaration" #>
     2.5    Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
     2.6      "equivariance theorem declaration (without checking the form of the lemma)" #>
     2.7 -  PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get);
     2.8 +  PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
     2.9  
    2.10  
    2.11  end;
     3.1 --- a/src/HOL/String.thy	Fri Aug 27 17:23:57 2010 +0200
     3.2 +++ b/src/HOL/String.thy	Fri Aug 27 17:59:40 2010 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
     3.5        nibbles nibbles;
     3.6  in
     3.7 -  PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     3.8 +  PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
     3.9    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    3.10  end
    3.11  *}
     4.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:23:57 2010 +0200
     4.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:59:40 2010 +0200
     4.3 @@ -679,9 +679,11 @@
     4.4  
     4.5  end;
     4.6  
     4.7 -val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
     4.8 -  (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
     4.9 -    (t, procedure t)))));
    4.10 +val (_, oracle) = Context.>>> (Context.map_theory_result
    4.11 +  (Thm.add_oracle (@{binding cooper},
    4.12 +    (fn (ctxt, t) =>
    4.13 +      (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
    4.14 +        (t, procedure t)))));
    4.15  
    4.16  val comp_ss = HOL_ss addsimps @{thms semiring_norm};
    4.17  
     5.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:23:57 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:59:40 2010 +0200
     5.3 @@ -310,18 +310,18 @@
     5.4  (* setup *)
     5.5  
     5.6  val setup =
     5.7 -  Attrib.setup (Binding.name "smt_solver")
     5.8 +  Attrib.setup @{binding smt_solver}
     5.9      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    5.10        (Thm.declaration_attribute o K o select_solver))
    5.11      "SMT solver configuration" #>
    5.12    setup_timeout #>
    5.13    setup_trace #>
    5.14    setup_fixed_certificates #>
    5.15 -  Attrib.setup (Binding.name "smt_certificates")
    5.16 +  Attrib.setup @{binding smt_certificates}
    5.17      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    5.18        (Thm.declaration_attribute o K o select_certificates))
    5.19      "SMT certificates" #>
    5.20 -  Method.setup (Binding.name "smt") smt_method
    5.21 +  Method.setup @{binding smt} smt_method
    5.22      "Applies an SMT solver to the current goal."
    5.23  
    5.24