src/Tools/induction.ML
changeset 67149 e61557884799
parent 61844 007d3b34080f
     1.1 --- a/src/Tools/induction.ML	Wed Dec 06 19:34:59 2017 +0100
     1.2 +++ b/src/Tools/induction.ML	Wed Dec 06 20:43:09 2017 +0100
     1.3 @@ -50,6 +50,6 @@
     1.4    Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
     1.5  
     1.6  val _ =
     1.7 -  Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic);
     1.8 +  Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);
     1.9  
    1.10  end