proper @{binding} antiquotations (relevant for formal references);
authorwenzelm
Fri Jul 01 15:16:03 2011 +0200 (2011-07-01)
changeset 436193803869014aa
parent 43618 1c43134ff988
child 43620 43a195a0279b
proper @{binding} antiquotations (relevant for formal references);
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/inductive_codegen.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/nbe.ML
src/Tools/value.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jul 01 15:14:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jul 01 15:16:03 2011 +0200
     1.3 @@ -1902,7 +1902,7 @@
     1.4      val setT = HOLogic.mk_setT T
     1.5      val elems = HOLogic.mk_set T ts
     1.6      val ([dots], ctxt') =
     1.7 -      Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix ("...", [], 1000))] ctxt 
     1.8 +      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt 
     1.9      (* check expected values *)
    1.10      val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
    1.11      val () =
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:14:44 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:16:03 2011 +0200
     2.3 @@ -408,8 +408,10 @@
     2.4          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
     2.5          val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
     2.6          val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
     2.7 -        val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
     2.8 -          ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
     2.9 +        (* FIXME proper naming convention for local_theory *)
    2.10 +        val ((prop_def, _), ctxt') =
    2.11 +          Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
    2.12 +            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    2.13          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    2.14          val (counterexample, result) = dynamic_value_strict (true, opts)
    2.15            (Existential_Counterexample.get, Existential_Counterexample.put,
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 15:14:44 2011 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 15:16:03 2011 +0200
     3.3 @@ -884,7 +884,7 @@
     3.4          val (_, thy') = Inductive.add_inductive_global
     3.5            {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
     3.6             no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
     3.7 -          [((Binding.name "quickcheckp", T), NoSyn)] []
     3.8 +          [((@{binding quickcheckp}, T), NoSyn)] []
     3.9            [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
    3.10          val pred = HOLogic.mk_Trueprop (list_comb
    3.11            (Const (Sign.intern_const thy' "quickcheckp", T),
     4.1 --- a/src/Tools/Code/code_runtime.ML	Fri Jul 01 15:14:44 2011 +0200
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Jul 01 15:16:03 2011 +0200
     4.3 @@ -163,7 +163,7 @@
     4.4    end;
     4.5  
     4.6  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
     4.7 -  (Thm.add_oracle (Binding.name "holds_by_evaluation",
     4.8 +  (Thm.add_oracle (@{binding holds_by_evaluation},
     4.9    fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
    4.10  
    4.11  fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
    4.12 @@ -338,7 +338,7 @@
    4.13  
    4.14  val _ =
    4.15    Context.>> (Context.map_theory
    4.16 -    (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
    4.17 +    (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
    4.18  
    4.19  local
    4.20  
     5.1 --- a/src/Tools/Code/code_simp.ML	Fri Jul 01 15:14:44 2011 +0200
     5.2 +++ b/src/Tools/Code/code_simp.ML	Fri Jul 01 15:16:03 2011 +0200
     5.3 @@ -58,9 +58,10 @@
     5.4  
     5.5  fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
     5.6  
     5.7 -val setup = Method.setup (Binding.name "code_simp")
     5.8 -  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
     5.9 -  "simplification with code equations"
    5.10 +val setup =
    5.11 +  Method.setup @{binding code_simp}
    5.12 +    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
    5.13 +    "simplification with code equations"
    5.14    #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
    5.15  
    5.16  
     6.1 --- a/src/Tools/nbe.ML	Fri Jul 01 15:14:44 2011 +0200
     6.2 +++ b/src/Tools/nbe.ML	Fri Jul 01 15:16:03 2011 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4  val get_triv_classes = map fst o Triv_Class_Data.get;
     6.5  
     6.6  val (_, triv_of_class) = Context.>>> (Context.map_theory_result
     6.7 -  (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
     6.8 +  (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
     6.9      Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
    6.10  
    6.11  in
    6.12 @@ -589,7 +589,7 @@
    6.13    in Thm.mk_binop eq lhs rhs end;
    6.14  
    6.15  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    6.16 -  (Thm.add_oracle (Binding.name "normalization_by_evaluation",
    6.17 +  (Thm.add_oracle (@{binding normalization_by_evaluation},
    6.18      fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
    6.19        mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
    6.20  
     7.1 --- a/src/Tools/value.ML	Fri Jul 01 15:14:44 2011 +0200
     7.2 +++ b/src/Tools/value.ML	Fri Jul 01 15:16:03 2011 +0200
     7.3 @@ -69,7 +69,7 @@
     7.4            (value_cmd some_name modes t)));
     7.5  
     7.6  val antiq_setup =
     7.7 -  Thy_Output.antiquotation (Binding.name "value")
     7.8 +  Thy_Output.antiquotation @{binding value}
     7.9      (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    7.10      (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    7.11        (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source