src/Pure/Isar/rule_insts.ML
changeset 52223 5bb6ae8acb87
parent 46476 dac966e4e51d
child 52732 b4da1f2ec73f
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   285     fun cvar xi = cert (Var (xi, propT));
   285     fun cvar xi = cert (Var (xi, propT));
   286     val revcut_rl' =
   286     val revcut_rl' =
   287       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   287       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   288         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   288         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   289   in
   289   in
   290     (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
   290     (case Seq.list_of
       
   291       (Thm.bicompose {flatten = true, match = false, incremented = false}
       
   292         (false, rl, Thm.nprems_of rl) 1 revcut_rl')
       
   293      of
   291       [th] => th
   294       [th] => th
   292     | _ => raise THM ("make_elim_preserve", 1, [rl]))
   295     | _ => raise THM ("make_elim_preserve", 1, [rl]))
   293   end;
   296   end;
   294 
   297 
   295 (*instantiate and cut -- for atomic fact*)
   298 (*instantiate and cut -- for atomic fact*)