src/ZF/Tools/induct_tacs.ML
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 27353 71c4dd53d4cb
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4               [] => error "induction is not available for this datatype"
     1.5             | major::_ => FOLogic.dest_Trueprop major)
     1.6    in
     1.7 -    RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
     1.8 +    eres_inst_tac ctxt [(ixn, var)] rule i state
     1.9    end
    1.10    handle Find_tname msg =>
    1.11              if exh then (*try boolean case analysis instead*)