--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Jan 04 23:22:53 2019 +0100
@@ -322,7 +322,7 @@
fun decomp_scnp_tac orders ctxt =
let
- val extra_simps = Named_Theorems.get ctxt @{named_theorems termination_simp}
+ val extra_simps = Named_Theorems.get ctxt \<^named_theorems>\<open>termination_simp\<close>
val autom_tac = auto_tac (ctxt addsimps extra_simps)
in
gen_sizechange_tac orders autom_tac ctxt
@@ -340,7 +340,7 @@
val _ =
Theory.setup
- (Method.setup @{binding size_change}
+ (Method.setup \<^binding>\<open>size_change\<close>
(Scan.lift orders --| Method.sections clasimp_modifiers >>
(fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
"termination prover with graph decomposition and the NP subset of size change termination")