src/ZF/Tools/induct_tacs.ML
changeset 36945 9bec62c10714
parent 36610 bafd82950e24
child 36954 ef698bd61057
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  fun exhaust_induct_tac exh ctxt var i state =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt
     1.7 -    val (_, _, Bi, _) = dest_state (state, i)
     1.8 +    val (_, _, Bi, _) = Thm.dest_state (state, i)
     1.9      val tn = find_tname var Bi
    1.10      val rule =
    1.11          if exh then #exhaustion (datatype_info thy tn)