src/Tools/eqsubst.ML
changeset 67149 e61557884799
parent 60358 aebfbcab1eb8
     1.1 --- a/src/Tools/eqsubst.ML	Wed Dec 06 19:34:59 2017 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Wed Dec 06 20:43:09 2017 +0100
     1.3 @@ -413,7 +413,7 @@
     1.4     the goal) as well as the theorems to use *)
     1.5  val _ =
     1.6    Theory.setup
     1.7 -    (Method.setup @{binding subst}
     1.8 +    (Method.setup \<^binding>\<open>subst\<close>
     1.9        (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
    1.10          Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
    1.11            SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))