src/HOL/HOL.thy
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 58958 114255dce178
     1.1 --- a/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -1463,7 +1463,7 @@
     1.4    val equal_def = @{thm induct_equal_def}
     1.5    fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     1.6      | dest_def _ = NONE
     1.7 -  val trivial_tac = match_tac @{thms induct_trueI}
     1.8 +  fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
     1.9  )
    1.10  *}
    1.11