src/HOL/Tools/inductive_set.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -114,9 +114,9 @@
     1.4              let val rews = map mk_rew ts
     1.5              in
     1.6                if forall is_none rews then NONE
     1.7 -              else SOME (fold (fn th1 => fn th2 => combination th2 th1)
     1.8 -                (map2 (fn SOME r => K r | NONE => reflexive o cterm_of thy)
     1.9 -                   rews ts) (reflexive (cterm_of thy h)))
    1.10 +              else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
    1.11 +                (map2 (fn SOME r => K r | NONE => Thm.reflexive o cterm_of thy)
    1.12 +                   rews ts) (Thm.reflexive (cterm_of thy h)))
    1.13              end
    1.14          | NONE => NONE)
    1.15        | _ => NONE