qualified constants Set.member and Set.Collect
authorhaftmann
Thu Jul 01 16:54:42 2010 +0200 (2010-07-01)
changeset 37677c5a8b612e571
parent 37676 f433cb9caea4
child 37678 0040bafffdef
qualified constants Set.member and Set.Collect
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Set.thy
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/refute.ML
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -3302,7 +3302,7 @@
     1.4    fun reorder_bounds_tac prems i =
     1.5      let
     1.6        fun variable_of_bound (Const ("Trueprop", _) $
     1.7 -                             (Const (@{const_name "op :"}, _) $
     1.8 +                             (Const (@{const_name Set.member}, _) $
     1.9                                Free (name, _) $ _)) = name
    1.10          | variable_of_bound (Const ("Trueprop", _) $
    1.11                               (Const ("op =", _) $
     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    | abs2list _ = [];
     2.5  
     2.6  (** maps {(x1,...,xn). t} to [x1,...,xn] **)
     2.7 -fun mk_vars (Const ("Collect",_) $ T) = abs2list T
     2.8 +fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
     2.9    | mk_vars _ = [];
    2.10  
    2.11  (** abstraction of body over a tuple formed from a list of free variables.
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jul 01 16:54:42 2010 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jul 01 16:54:42 2010 +0200
     3.3 @@ -2088,7 +2088,7 @@
     3.4              val (HOLThm(rens,td_th)) = norm_hthm thy hth
     3.5              val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
     3.6              val c = case concl_of th2 of
     3.7 -                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
     3.8 +                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
     3.9                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
    3.10              val tfrees = OldTerm.term_tfrees c
    3.11              val tnames = map fst tfrees
    3.12 @@ -2118,7 +2118,7 @@
    3.13                            let
    3.14                                val PT = domain_type exT
    3.15                            in
    3.16 -                              Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
    3.17 +                              Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P
    3.18                            end
    3.19                          | _ => error "Internal error in ProofKernel.new_typedefinition"
    3.20              val tnames_string = if null tnames
    3.21 @@ -2164,7 +2164,7 @@
    3.22                                      SOME (cterm_of thy t)] light_nonempty
    3.23              val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
    3.24              val c = case concl_of th2 of
    3.25 -                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
    3.26 +                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
    3.27                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
    3.28              val tfrees = OldTerm.term_tfrees c
    3.29              val tnames = sort_strings (map fst tfrees)
    3.30 @@ -2202,7 +2202,7 @@
    3.31                  let
    3.32                      val PT = type_of P'
    3.33                  in
    3.34 -                    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
    3.35 +                    Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P'
    3.36                  end
    3.37  
    3.38              val tnames_string = if null tnames
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 01 16:54:42 2010 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 01 16:54:42 2010 +0200
     4.3 @@ -121,7 +121,7 @@
     4.4  
     4.5  val dj_cp = thm "dj_cp";
     4.6  
     4.7 -fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
     4.8 +fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
     4.9        Type ("fun", [_, U])])) = (T, U);
    4.10  
    4.11  fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    4.12 @@ -617,7 +617,7 @@
    4.13        |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
    4.14            Typedef.add_typedef_global false (SOME (Binding.name name'))
    4.15              (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    4.16 -            (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    4.17 +            (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    4.18                 Const (cname, U --> HOLogic.boolT)) NONE
    4.19              (rtac exI 1 THEN rtac CollectI 1 THEN
    4.20                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     5.1 --- a/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
     5.2 +++ b/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
     5.3 @@ -8,42 +8,36 @@
     5.4  
     5.5  subsection {* Sets as predicates *}
     5.6  
     5.7 -global
     5.8 -
     5.9 -types 'a set = "'a => bool"
    5.10 +types 'a set = "'a \<Rightarrow> bool"
    5.11  
    5.12 -consts
    5.13 -  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    5.14 -  "op :"        :: "'a => 'a set => bool"                -- "membership"
    5.15 +definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
    5.16 +  "Collect P = P"
    5.17  
    5.18 -local
    5.19 +definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
    5.20 +  mem_def: "member x A = A x"
    5.21  
    5.22  notation
    5.23 -  "op :"  ("op :") and
    5.24 -  "op :"  ("(_/ : _)" [50, 51] 50)
    5.25 +  member  ("op :") and
    5.26 +  member  ("(_/ : _)" [50, 51] 50)
    5.27  
    5.28 -defs
    5.29 -  mem_def [code]: "x : S == S x"
    5.30 -  Collect_def [code]: "Collect P == P"
    5.31 -
    5.32 -abbreviation
    5.33 -  "not_mem x A == ~ (x : A)" -- "non-membership"
    5.34 +abbreviation not_member where
    5.35 +  "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
    5.36  
    5.37  notation
    5.38 -  not_mem  ("op ~:") and
    5.39 -  not_mem  ("(_/ ~: _)" [50, 51] 50)
    5.40 +  not_member  ("op ~:") and
    5.41 +  not_member  ("(_/ ~: _)" [50, 51] 50)
    5.42  
    5.43  notation (xsymbols)
    5.44 -  "op :"  ("op \<in>") and
    5.45 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
    5.46 -  not_mem  ("op \<notin>") and
    5.47 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
    5.48 +  member      ("op \<in>") and
    5.49 +  member      ("(_/ \<in> _)" [50, 51] 50) and
    5.50 +  not_member  ("op \<notin>") and
    5.51 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    5.52  
    5.53  notation (HTML output)
    5.54 -  "op :"  ("op \<in>") and
    5.55 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
    5.56 -  not_mem  ("op \<notin>") and
    5.57 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
    5.58 +  member      ("op \<in>") and
    5.59 +  member      ("(_/ \<in> _)" [50, 51] 50) and
    5.60 +  not_member  ("op \<notin>") and
    5.61 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    5.62  
    5.63  text {* Set comprehensions *}
    5.64  
    5.65 @@ -312,7 +306,7 @@
    5.66          in
    5.67            case t of
    5.68              Const (@{const_syntax "op &"}, _) $
    5.69 -              (Const (@{const_syntax "op :"}, _) $
    5.70 +              (Const (@{const_syntax Set.member}, _) $
    5.71                  (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
    5.72              if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
    5.73            | _ => M
    5.74 @@ -922,7 +916,7 @@
    5.75  lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
    5.76  
    5.77  (*Would like to add these, but the existing code only searches for the
    5.78 -  outer-level constant, which in this case is just "op :"; we instead need
    5.79 +  outer-level constant, which in this case is just Set.member; we instead need
    5.80    to use term-nets to associate patterns with rules.  Also, if a rule fails to
    5.81    apply, then the formula should be kept.
    5.82    [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
    5.83 @@ -1691,6 +1685,7 @@
    5.84  lemma vimage_code [code]: "(f -` A) x = A (f x)"
    5.85    by (simp add: vimage_def Collect_def mem_def)
    5.86  
    5.87 +hide_const (open) member
    5.88  
    5.89  text {* Misc theorem and ML bindings *}
    5.90  
     6.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
     6.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
     6.3 @@ -220,7 +220,7 @@
     6.4      val ihyp = Term.all T $ Abs ("z", T,
     6.5        Logic.mk_implies
     6.6          (HOLogic.mk_Trueprop (
     6.7 -          Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
     6.8 +          Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
     6.9            $ (HOLogic.pair_const T T $ Bound 0 $ x)
    6.10            $ R),
    6.11           HOLogic.mk_Trueprop (P_comp $ Bound 0)))
     7.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 01 16:54:42 2010 +0200
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 01 16:54:42 2010 +0200
     7.3 @@ -54,15 +54,15 @@
     7.4  fun negF AbsF = RepF
     7.5    | negF RepF = AbsF
     7.6  
     7.7 -fun is_identity (Const (@{const_name "id"}, _)) = true
     7.8 +fun is_identity (Const (@{const_name id}, _)) = true
     7.9    | is_identity _ = false
    7.10  
    7.11 -fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
    7.12 +fun mk_identity ty = Const (@{const_name id}, ty --> ty)
    7.13  
    7.14  fun mk_fun_compose flag (trm1, trm2) =
    7.15    case flag of
    7.16 -    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
    7.17 -  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
    7.18 +    AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
    7.19 +  | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
    7.20  
    7.21  fun get_mapfun ctxt s =
    7.22  let
    7.23 @@ -450,7 +450,7 @@
    7.24           if ty = ty' then subtrm
    7.25           else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
    7.26         end
    7.27 -  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
    7.28 +  | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
    7.29         let
    7.30           val subtrm = regularize_trm ctxt (t, t')
    7.31           val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
    7.32 @@ -460,26 +460,26 @@
    7.33           else mk_babs $ resrel $ subtrm
    7.34         end
    7.35  
    7.36 -  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
    7.37 +  | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
    7.38         let
    7.39           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    7.40         in
    7.41 -         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
    7.42 +         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
    7.43           else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
    7.44         end
    7.45  
    7.46 -  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
    7.47 +  | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
    7.48         let
    7.49           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    7.50         in
    7.51 -         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
    7.52 +         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
    7.53           else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
    7.54         end
    7.55  
    7.56 -  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
    7.57 -      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
    7.58 -        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
    7.59 -     Const (@{const_name "Ex1"}, ty') $ t') =>
    7.60 +  | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
    7.61 +      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
    7.62 +        (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
    7.63 +     Const (@{const_name Ex1}, ty') $ t') =>
    7.64         let
    7.65           val t_ = incr_boundvars (~1) t
    7.66           val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
     8.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jul 01 16:54:42 2010 +0200
     8.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jul 01 16:54:42 2010 +0200
     8.3 @@ -579,7 +579,7 @@
     8.4        fun get_nparms s = if member (op =) names s then SOME nparms else
     8.5          Option.map #3 (get_clauses thy s);
     8.6  
     8.7 -      fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
     8.8 +      fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
     8.9              Prem ([t], Envir.beta_eta_contract u, true)
    8.10          | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
    8.11              Prem ([t, u], eq, false)
     9.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Jul 01 16:54:42 2010 +0200
     9.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Jul 01 16:54:42 2010 +0200
     9.3 @@ -36,7 +36,7 @@
     9.4      fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
     9.5           let val (u, _, ps) = HOLogic.strip_psplits t
     9.6           in case u of
     9.7 -           (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
     9.8 +           (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
     9.9               (case try (HOLogic.strip_ptuple ps) q of
    9.10                  NONE => NONE
    9.11                | SOME ts =>
    9.12 @@ -84,10 +84,10 @@
    9.13          in HOLogic.Collect_const U $
    9.14            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    9.15          end;
    9.16 -      fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
    9.17 +      fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
    9.18              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    9.19                mkop s T (m, p, S, mk_collect p T (head_of u))
    9.20 -        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
    9.21 +        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member},
    9.22              Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
    9.23                mkop s T (m, p, mk_collect p T (head_of u), S)
    9.24          | decomp _ = NONE;
    9.25 @@ -271,7 +271,7 @@
    9.26             let
    9.27               val thy = Context.theory_of ctxt;
    9.28               fun factors_of t fs = case strip_abs_body t of
    9.29 -                 Const (@{const_name "op :"}, _) $ u $ S =>
    9.30 +                 Const (@{const_name Set.member}, _) $ u $ S =>
    9.31                     if is_Free S orelse is_Var S then
    9.32                       let val ps = HOLogic.flat_tuple_paths u
    9.33                       in (SOME ps, (S, ps) :: fs) end
    9.34 @@ -281,7 +281,7 @@
    9.35               val (pfs, fs) = fold_map factors_of ts [];
    9.36               val ((h', ts'), fs') = (case rhs of
    9.37                   Abs _ => (case strip_abs_body rhs of
    9.38 -                     Const (@{const_name "op :"}, _) $ u $ S =>
    9.39 +                     Const (@{const_name Set.member}, _) $ u $ S =>
    9.40                         (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
    9.41                     | _ => error "member symbol on right-hand side expected")
    9.42                 | _ => (strip_comb rhs, NONE))
    9.43 @@ -414,7 +414,7 @@
    9.44      val {set_arities, pred_arities, to_pred_simps, ...} =
    9.45        PredSetConvData.get (Context.Proof lthy);
    9.46      fun infer (Abs (_, _, t)) = infer t
    9.47 -      | infer (Const (@{const_name "op :"}, _) $ t $ u) =
    9.48 +      | infer (Const (@{const_name Set.member}, _) $ t $ u) =
    9.49            infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
    9.50        | infer (t $ u) = infer t #> infer u
    9.51        | infer _ = I;
    10.1 --- a/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
    10.2 +++ b/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
    10.3 @@ -653,7 +653,7 @@
    10.4        | Const (@{const_name "op -->"}, _) => t
    10.5        (* sets *)
    10.6        | Const (@{const_name Collect}, _) => t
    10.7 -      | Const (@{const_name "op :"}, _) => t
    10.8 +      | Const (@{const_name Set.member}, _) => t
    10.9        (* other optimizations *)
   10.10        | Const (@{const_name Finite_Set.card}, _) => t
   10.11        | Const (@{const_name Finite_Set.finite}, _) => t
   10.12 @@ -829,7 +829,7 @@
   10.13        | Const (@{const_name "op -->"}, _) => axs
   10.14        (* sets *)
   10.15        | Const (@{const_name Collect}, T) => collect_type_axioms T axs
   10.16 -      | Const (@{const_name "op :"}, T) => collect_type_axioms T axs
   10.17 +      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
   10.18        (* other optimizations *)
   10.19        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   10.20        | Const (@{const_name Finite_Set.finite}, T) =>
   10.21 @@ -2634,11 +2634,11 @@
   10.22        | Const (@{const_name Collect}, _) =>
   10.23          SOME (interpret thy model args (eta_expand t 1))
   10.24        (* 'op :' == application *)
   10.25 -      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
   10.26 +      | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
   10.27          SOME (interpret thy model args (t2 $ t1))
   10.28 -      | Const (@{const_name "op :"}, _) $ t1 =>
   10.29 +      | Const (@{const_name Set.member}, _) $ t1 =>
   10.30          SOME (interpret thy model args (eta_expand t 1))
   10.31 -      | Const (@{const_name "op :"}, _) =>
   10.32 +      | Const (@{const_name Set.member}, _) =>
   10.33          SOME (interpret thy model args (eta_expand t 2))
   10.34        | _ => NONE)
   10.35    end;
   10.36 @@ -3050,7 +3050,7 @@
   10.37  
   10.38    fun Product_Type_fst_interpreter thy model args t =
   10.39      case t of
   10.40 -      Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
   10.41 +      Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
   10.42        let
   10.43          val constants_T = make_constants thy model T
   10.44          val size_U      = size_of_type thy model U
   10.45 @@ -3069,7 +3069,7 @@
   10.46  
   10.47    fun Product_Type_snd_interpreter thy model args t =
   10.48      case t of
   10.49 -      Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
   10.50 +      Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
   10.51        let
   10.52          val size_T      = size_of_type thy model T
   10.53          val constants_U = make_constants thy model U
    11.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
    11.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
    11.3 @@ -858,7 +858,7 @@
    11.4    val rtrancl_trans = @{thm rtrancl_trans};
    11.5  
    11.6    fun decomp (@{const Trueprop} $ t) =
    11.7 -    let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
    11.8 +    let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
    11.9          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
   11.10                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
   11.11                | decr r = (r,"r");