src/HOL/Tools/Function/induction_schema.ML
changeset 58950 d07464875dd4
parent 55968 94242fa87638
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -387,7 +387,7 @@
     1.4      val nbranches = length branches
     1.5      val npres = length pres
     1.6    in
     1.7 -    Thm.bicompose {flatten = false, match = false, incremented = false}
     1.8 +    Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
     1.9        (false, res, length newgoals) i
    1.10      THEN term_tac (i + nbranches + npres)
    1.11      THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))