src/HOL/Tools/inductive_set.ML
changeset 35364 b8c62d60195c
parent 34986 7f7939c9370f
child 35646 b32d6c1bdb4d
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Feb 25 22:17:33 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Feb 25 22:32:09 2010 +0100
     1.3 @@ -33,10 +33,10 @@
     1.4  
     1.5  val collect_mem_simproc =
     1.6    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     1.7 -    fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
     1.8 +    fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
     1.9           let val (u, _, ps) = HOLogic.strip_psplits t
    1.10           in case u of
    1.11 -           (c as Const ("op :", _)) $ q $ S' =>
    1.12 +           (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
    1.13               (case try (HOLogic.strip_ptuple ps) q of
    1.14                  NONE => NONE
    1.15                | SOME ts =>
    1.16 @@ -74,18 +74,20 @@
    1.17          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    1.18            (p (fold (Logic.all o Var) vs t) f)
    1.19          end;
    1.20 -      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
    1.21 -        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
    1.22 +      fun mkop @{const_name "op &"} T x =
    1.23 +            SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
    1.24 +        | mkop @{const_name "op |"} T x =
    1.25 +            SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
    1.26          | mkop _ _ _ = NONE;
    1.27        fun mk_collect p T t =
    1.28          let val U = HOLogic.dest_setT T
    1.29          in HOLogic.Collect_const U $
    1.30            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    1.31          end;
    1.32 -      fun decomp (Const (s, _) $ ((m as Const ("op :",
    1.33 +      fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
    1.34              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    1.35                mkop s T (m, p, S, mk_collect p T (head_of u))
    1.36 -        | decomp (Const (s, _) $ u $ ((m as Const ("op :",
    1.37 +        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
    1.38              Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
    1.39                mkop s T (m, p, mk_collect p T (head_of u), S)
    1.40          | decomp _ = NONE;
    1.41 @@ -263,13 +265,13 @@
    1.42  
    1.43  fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
    1.44    case prop_of thm of
    1.45 -    Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) =>
    1.46 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
    1.47        (case body_type T of
    1.48 -         Type ("bool", []) =>
    1.49 +         @{typ bool} =>
    1.50             let
    1.51               val thy = Context.theory_of ctxt;
    1.52               fun factors_of t fs = case strip_abs_body t of
    1.53 -                 Const ("op :", _) $ u $ S =>
    1.54 +                 Const (@{const_name "op :"}, _) $ u $ S =>
    1.55                     if is_Free S orelse is_Var S then
    1.56                       let val ps = HOLogic.flat_tuple_paths u
    1.57                       in (SOME ps, (S, ps) :: fs) end
    1.58 @@ -279,7 +281,7 @@
    1.59               val (pfs, fs) = fold_map factors_of ts [];
    1.60               val ((h', ts'), fs') = (case rhs of
    1.61                   Abs _ => (case strip_abs_body rhs of
    1.62 -                     Const ("op :", _) $ u $ S =>
    1.63 +                     Const (@{const_name "op :"}, _) $ u $ S =>
    1.64                         (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
    1.65                     | _ => error "member symbol on right-hand side expected")
    1.66                 | _ => (strip_comb rhs, NONE))
    1.67 @@ -412,7 +414,7 @@
    1.68      val {set_arities, pred_arities, to_pred_simps, ...} =
    1.69        PredSetConvData.get (Context.Proof lthy);
    1.70      fun infer (Abs (_, _, t)) = infer t
    1.71 -      | infer (Const ("op :", _) $ t $ u) =
    1.72 +      | infer (Const (@{const_name "op :"}, _) $ t $ u) =
    1.73            infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
    1.74        | infer (t $ u) = infer t #> infer u
    1.75        | infer _ = I;