src/HOL/Tools/inductive_set.ML
changeset 32603 e08fdd615333
parent 32351 96f9e6402403
child 32683 7c1fe854ca6a
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:50 2009 +0200
     1.3 @@ -74,8 +74,8 @@
     1.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
     1.5            (p (fold (Logic.all o Var) vs t) f)
     1.6          end;
     1.7 -      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
     1.8 -        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
     1.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
    1.10 +        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
    1.11          | mkop _ _ _ = NONE;
    1.12        fun mk_collect p T t =
    1.13          let val U = HOLogic.dest_setT T