src/Pure/Isar/method.ML
changeset 19046 bc5c6c9b114e
parent 18999 e0eb9cb97db0
child 19186 1bf4b5c4a794
     1.1 --- a/src/Pure/Isar/method.ML	Wed Feb 15 19:11:10 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Feb 15 21:34:55 2006 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4  
     1.5  val remdups_tac = SUBGOAL (fn (g, i) =>
     1.6    let val prems = Logic.strip_assums_hyp g in
     1.7 -    REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
     1.8 +    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
     1.9      (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    1.10    end);
    1.11  
    1.12 @@ -393,7 +393,7 @@
    1.13            map
    1.14              (fn (xi, t) =>
    1.15                pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
    1.16 -            (gen_distinct
    1.17 +            (distinct
    1.18                (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
    1.19                (xis ~~ ts));
    1.20          (* Lift and instantiate rule *)