src/Pure/Isar/rule_insts.ML
changeset 31945 d5f186aa0bed
parent 30763 6976521b4263
child 31977 e03059ae2d82
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -354,7 +354,7 @@
     1.4        instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
     1.5          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
     1.6    in
     1.7 -    (case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
     1.8 +    (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
     1.9        [th] => th
    1.10      | _ => raise THM ("make_elim_preserve", 1, [rl]))
    1.11    end;