avoid unnamed infixes;
authorwenzelm
Wed Oct 03 22:33:17 2007 +0200 (2007-10-03)
changeset 2482678e6a3cea367
parent 24825 c4f13ab78f9d
child 24827 646bdc51eb7d
avoid unnamed infixes;
src/ZF/Inductive.thy
src/ZF/OrderType.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
src/ZF/ZF.thy
src/ZF/ind_syntax.ML
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/Inductive.thy	Wed Oct 03 21:29:05 2007 +0200
     1.2 +++ b/src/ZF/Inductive.thy	Wed Oct 03 22:33:17 2007 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  structure Standard_Sum =
     1.6    struct
     1.7 -  val sum       = Const("op +", [iT,iT]--->iT)
     1.8 +  val sum       = Const(@{const_name sum}, [iT,iT]--->iT)
     1.9    val inl       = Const("Inl", iT-->iT)
    1.10    val inr       = Const("Inr", iT-->iT)
    1.11    val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
     2.1 --- a/src/ZF/OrderType.thy	Wed Oct 03 21:29:05 2007 +0200
     2.2 +++ b/src/ZF/OrderType.thy	Wed Oct 03 22:33:17 2007 +0200
     2.3 @@ -45,11 +45,11 @@
     2.4      "i -- j == ordertype(i-j, Memrel(i))"
     2.5  
     2.6    
     2.7 -syntax (xsymbols)
     2.8 -  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
     2.9 +notation (xsymbols)
    2.10 +  omult  (infixl "\<times>\<times>" 70)
    2.11  
    2.12 -syntax (HTML output)
    2.13 -  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
    2.14 +notation (HTML output)
    2.15 +  omult  (infixl "\<times>\<times>" 70)
    2.16  
    2.17  
    2.18  subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
     3.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Oct 03 21:29:05 2007 +0200
     3.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Oct 03 22:33:17 2007 +0200
     3.3 @@ -174,7 +174,7 @@
     3.4  
     3.5    (*Find each recursive argument and add a recursive call for it*)
     3.6    fun rec_args [] = []
     3.7 -    | rec_args ((Const("op :",_)$arg$X)::prems) =
     3.8 +    | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
     3.9         (case head_of X of
    3.10              Const(a,_) => (*recursive occurrence?*)
    3.11                            if a mem_string rec_names
    3.12 @@ -293,7 +293,7 @@
    3.13     | SOME recursor_def =>
    3.14        let
    3.15          (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
    3.16 -        fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
    3.17 +        fun subst_rec (Const(@{const_name apply},_) $ Free _ $ arg) = recursor_tm $ arg
    3.18            | subst_rec tm =
    3.19                let val (head, args) = strip_comb tm
    3.20                in  list_comb (head, map subst_rec args)  end;
     4.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Oct 03 21:29:05 2007 +0200
     4.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Oct 03 22:33:17 2007 +0200
     4.3 @@ -72,7 +72,7 @@
     4.4  exception Find_tname of string
     4.5  
     4.6  fun find_tname var Bi =
     4.7 -  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
     4.8 +  let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
     4.9               (v, #1 (dest_Const (head_of A)))
    4.10          | mk_pair _ = raise Match
    4.11        val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
    4.12 @@ -97,7 +97,7 @@
    4.13      val rule =
    4.14          if exh then #exhaustion (datatype_info thy tn)
    4.15                 else #induct  (datatype_info thy tn)
    4.16 -    val (Const("op :",_) $ Var(ixn,_) $ _) =
    4.17 +    val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) =
    4.18          (case prems_of rule of
    4.19               [] => error "induction is not available for this datatype"
    4.20             | major::_ => FOLogic.dest_Trueprop major)
    4.21 @@ -126,7 +126,7 @@
    4.22          map (head_of o const_of o FOLogic.dest_Trueprop o
    4.23               #prop o rep_thm) case_eqns;
    4.24  
    4.25 -    val Const ("op :", _) $ _ $ data =
    4.26 +    val Const (@{const_name mem}, _) $ _ $ data =
    4.27          FOLogic.dest_Trueprop (hd (prems_of elim));
    4.28  
    4.29      val Const(big_rec_name, _) = head_of data;
     5.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Oct 03 21:29:05 2007 +0200
     5.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Oct 03 22:33:17 2007 +0200
     5.3 @@ -286,7 +286,7 @@
     5.4          ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
     5.5          prem is a premise of an intr rule*)
     5.6       fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
     5.7 -                      (Const("op :",_)$t$X), iprems) =
     5.8 +                      (Const(@{const_name mem},_)$t$X), iprems) =
     5.9            (case AList.lookup (op aconv) ind_alist X of
    5.10                 SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
    5.11               | NONE => (*possibly membership in M(rec_tm), for M monotone*)
     6.1 --- a/src/ZF/Tools/typechk.ML	Wed Oct 03 21:29:05 2007 +0200
     6.2 +++ b/src/ZF/Tools/typechk.ML	Wed Oct 03 22:33:17 2007 +0200
     6.3 @@ -76,7 +76,7 @@
     6.4           if length rls <= maxr then resolve_tac rls i else no_tac
     6.5        end);
     6.6  
     6.7 -fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
     6.8 +fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
     6.9        not (is_Var (head_of a))
    6.10    | is_rigid_elem _ = false;
    6.11  
     7.1 --- a/src/ZF/ZF.thy	Wed Oct 03 21:29:05 2007 +0200
     7.2 +++ b/src/ZF/ZF.thy	Wed Oct 03 22:33:17 2007 +0200
     7.3 @@ -43,11 +43,9 @@
     7.4    The         :: "(i => o) => i"      (binder "THE " 10)
     7.5    If          :: "[o, i, i] => i"     ("(if (_)/ then (_)/ else (_))" [10] 10)
     7.6  
     7.7 -syntax
     7.8 -  old_if      :: "[o, i, i] => i"   ("if '(_,_,_')")
     7.9 -
    7.10 -translations
    7.11 -  "if(P,a,b)" => "If(P,a,b)"
    7.12 +abbreviation (input)
    7.13 +  old_if      :: "[o, i, i] => i"   ("if '(_,_,_')") where
    7.14 +  "if(P,a,b) == If(P,a,b)"
    7.15  
    7.16  
    7.17  text {*Finite Sets *}
    7.18 @@ -75,24 +73,33 @@
    7.19    field       :: "i => i"
    7.20    converse    :: "i => i"
    7.21    relation    :: "i => o"        --{*recognizes sets of pairs*}
    7.22 -  function    :: "i => o"        --{*recognizes functions; can have non-pairs*}
    7.23 +  "function"  :: "i => o"        --{*recognizes functions; can have non-pairs*}
    7.24    Lambda      :: "[i, i => i] => i"
    7.25    restrict    :: "[i, i] => i"
    7.26  
    7.27  text {*Infixes in order of decreasing precedence *}
    7.28  consts
    7.29  
    7.30 -  "``"        :: "[i, i] => i"    (infixl 90) --{*image*}
    7.31 -  "-``"       :: "[i, i] => i"    (infixl 90) --{*inverse image*}
    7.32 -  "`"         :: "[i, i] => i"    (infixl 90) --{*function application*}
    7.33 -(*"*"         :: "[i, i] => i"    (infixr 80) [virtual] Cartesian product*)
    7.34 -  "Int"       :: "[i, i] => i"    (infixl 70) --{*binary intersection*}
    7.35 -  "Un"        :: "[i, i] => i"    (infixl 65) --{*binary union*}
    7.36 -  "-"         :: "[i, i] => i"    (infixl 65) --{*set difference*}
    7.37 -(*"->"        :: "[i, i] => i"    (infixr 60) [virtual] function spac\<epsilon>*)
    7.38 -  "<="        :: "[i, i] => o"    (infixl 50) --{*subset relation*}
    7.39 -  ":"         :: "[i, i] => o"    (infixl 50) --{*membership relation*}
    7.40 -(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
    7.41 +  Image       :: "[i, i] => i"    (infixl "``" 90) --{*image*}
    7.42 +  vimage      :: "[i, i] => i"    (infixl "-``" 90) --{*inverse image*}
    7.43 +  "apply"     :: "[i, i] => i"    (infixl "`" 90) --{*function application*}
    7.44 +  "Int"       :: "[i, i] => i"    (infixl "Int" 70) --{*binary intersection*}
    7.45 +  "Un"        :: "[i, i] => i"    (infixl "Un" 65) --{*binary union*}
    7.46 +  Diff        :: "[i, i] => i"    (infixl "-" 65) --{*set difference*}
    7.47 +  Subset      :: "[i, i] => o"    (infixl "<=" 50) --{*subset relation*}
    7.48 +  mem         :: "[i, i] => o"    (infixl ":" 50) --{*membership relation*}
    7.49 +
    7.50 +abbreviation
    7.51 +  not_mem :: "[i, i] => o"  (infixl "~:" 50)  --{*negated membership relation*}
    7.52 +  where "x ~: y == ~ (x : y)"
    7.53 +
    7.54 +abbreviation
    7.55 +  cart_prod :: "[i, i] => i"    (infixr "*" 80) --{*Cartesian product*}
    7.56 +  where "A * B == Sigma(A, %_. B)"
    7.57 +
    7.58 +abbreviation
    7.59 +  function_space :: "[i, i] => i"  (infixr "->" 60) --{*function space*}
    7.60 +  where "A -> B == Pi(A, %_. B)"
    7.61  
    7.62  
    7.63  nonterminals "is" patterns
    7.64 @@ -100,7 +107,7 @@
    7.65  syntax
    7.66    ""          :: "i => is"                   ("_")
    7.67    "@Enum"     :: "[i, is] => is"             ("_,/ _")
    7.68 -  "~:"        :: "[i, i] => o"               (infixl 50)
    7.69 +
    7.70    "@Finset"   :: "is => i"                   ("{(_)}")
    7.71    "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
    7.72    "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
    7.73 @@ -110,8 +117,6 @@
    7.74    "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
    7.75    "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
    7.76    "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
    7.77 -  "->"        :: "[i, i] => i"               (infixr 60)
    7.78 -  "*"         :: "[i, i] => i"               (infixr 80)
    7.79    "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
    7.80    "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
    7.81    "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
    7.82 @@ -123,7 +128,6 @@
    7.83    "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
    7.84  
    7.85  translations
    7.86 -  "x ~: y"      == "~ (x : y)"
    7.87    "{x, xs}"     == "cons(x, {xs})"
    7.88    "{x}"         == "cons(x, 0)"
    7.89    "{x:A. P}"    == "Collect(A, %x. P)"
    7.90 @@ -131,10 +135,8 @@
    7.91    "{b. x:A}"    == "RepFun(A, %x. b)"
    7.92    "INT x:A. B"  == "Inter({B. x:A})"
    7.93    "UN x:A. B"   == "Union({B. x:A})"
    7.94 -  "PROD x:A. B" => "Pi(A, %x. B)"
    7.95 -  "SUM x:A. B"  => "Sigma(A, %x. B)"
    7.96 -  "A -> B"      => "Pi(A, %_. B)"
    7.97 -  "A * B"       => "Sigma(A, %_. B)"
    7.98 +  "PROD x:A. B" == "Pi(A, %x. B)"
    7.99 +  "SUM x:A. B"  == "Sigma(A, %x. B)"
   7.100    "lam x:A. f"  == "Lambda(A, %x. f)"
   7.101    "ALL x:A. P"  == "Ball(A, %x. P)"
   7.102    "EX x:A. P"   == "Bex(A, %x. P)"
   7.103 @@ -145,21 +147,23 @@
   7.104    "%<x,y>.b"    == "split(%x y. b)"
   7.105  
   7.106  
   7.107 +notation (xsymbols)
   7.108 +  cart_prod       (infixr "\<times>" 80) and
   7.109 +  Int             (infixl "\<inter>" 70) and
   7.110 +  Un              (infixl "\<union>" 65) and
   7.111 +  function_space  (infixr "\<rightarrow>" 60) and
   7.112 +  Subset          (infixl "\<subseteq>" 50) and
   7.113 +  mem             (infixl "\<in>" 50) and
   7.114 +  not_mem         (infixl "\<notin>" 50) and
   7.115 +  Union           ("\<Union>_" [90] 90) and
   7.116 +  Inter           ("\<Inter>_" [90] 90)
   7.117 +
   7.118  syntax (xsymbols)
   7.119 -  "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
   7.120 -  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
   7.121 -  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
   7.122 -  "op ->"     :: "[i, i] => i"               (infixr "\<rightarrow>" 60)
   7.123 -  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
   7.124 -  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
   7.125 -  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
   7.126    "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
   7.127    "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
   7.128    "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
   7.129    "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
   7.130    "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
   7.131 -  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
   7.132 -  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
   7.133    "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
   7.134    "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
   7.135    "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   7.136 @@ -168,20 +172,22 @@
   7.137    "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
   7.138    "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   7.139  
   7.140 +notation (HTML output)
   7.141 +  cart_prod       (infixr "\<times>" 80) and
   7.142 +  Int             (infixl "\<inter>" 70) and
   7.143 +  Un              (infixl "\<union>" 65) and
   7.144 +  Subset          (infixl "\<subseteq>" 50) and
   7.145 +  mem             (infixl "\<in>" 50) and
   7.146 +  not_mem         (infixl "\<notin>" 50) and
   7.147 +  Union           ("\<Union>_" [90] 90) and
   7.148 +  Inter           ("\<Inter>_" [90] 90)
   7.149 +
   7.150  syntax (HTML output)
   7.151 -  "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
   7.152 -  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
   7.153 -  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
   7.154 -  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
   7.155 -  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
   7.156 -  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
   7.157    "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
   7.158    "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
   7.159    "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
   7.160    "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
   7.161    "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
   7.162 -  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
   7.163 -  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
   7.164    "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
   7.165    "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
   7.166    "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   7.167 @@ -192,8 +198,7 @@
   7.168  
   7.169  
   7.170  finalconsts
   7.171 -  0 Pow Inf Union PrimReplace 
   7.172 -  "op :"
   7.173 +  0 Pow Inf Union PrimReplace mem
   7.174  
   7.175  defs 
   7.176  (*don't try to use constdefs: the declaration order is tightly constrained*)
   7.177 @@ -293,12 +298,6 @@
   7.178    (* Restrict the relation r to the domain A *)
   7.179    restrict_def: "restrict(r,A) == {z : r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
   7.180  
   7.181 -(* Pattern-matching and 'Dependent' type operators *)
   7.182 -
   7.183 -print_translation {*
   7.184 -  [("Pi",    dependent_tr' ("@PROD", "op ->")),
   7.185 -   ("Sigma", dependent_tr' ("@SUM", "op *"))];
   7.186 -*}
   7.187  
   7.188  subsection {* Substitution*}
   7.189  
     8.1 --- a/src/ZF/ind_syntax.ML	Wed Oct 03 21:29:05 2007 +0200
     8.2 +++ b/src/ZF/ind_syntax.ML	Wed Oct 03 22:33:17 2007 +0200
     8.3 @@ -24,7 +24,7 @@
     8.4  
     8.5  val iT = Type("i",[]);
     8.6  
     8.7 -val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
     8.8 +val mem_const = @{term mem};
     8.9  
    8.10  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    8.11  fun mk_all_imp (A,P) = 
    8.12 @@ -34,7 +34,7 @@
    8.13  
    8.14  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    8.15  
    8.16 -val apply_const = Const("op `", [iT,iT]--->iT);
    8.17 +val apply_const = @{term apply};
    8.18  
    8.19  val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    8.20  
    8.21 @@ -44,14 +44,14 @@
    8.22  (*simple error-checking in the premises of an inductive definition*)
    8.23  fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    8.24          error"Premises may not be conjuctive"
    8.25 -  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    8.26 +  | chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) = 
    8.27          (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
    8.28    | chk_prem rec_hd t = 
    8.29          (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
    8.30  
    8.31  (*Return the conclusion of a rule, of the form t:X*)
    8.32  fun rule_concl rl = 
    8.33 -    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
    8.34 +    let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) = 
    8.35                  Logic.strip_imp_concl rl
    8.36      in  (t,X)  end;
    8.37  
    8.38 @@ -74,7 +74,7 @@
    8.39  type constructor_spec = 
    8.40      ((string * typ * mixfix) * string * term list * term list);
    8.41  
    8.42 -fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    8.43 +fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
    8.44    | dest_mem _ = error "Constructor specifications must have the form x:A";
    8.45  
    8.46  (*read a constructor specification*)
    8.47 @@ -102,7 +102,7 @@
    8.48  
    8.49  fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
    8.50  
    8.51 -fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
    8.52 +fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
    8.53  
    8.54  val empty       = Const("0", iT)
    8.55  and univ        = Const("Univ.univ", iT-->iT)
     9.1 --- a/src/ZF/simpdata.ML	Wed Oct 03 21:29:05 2007 +0200
     9.2 +++ b/src/ZF/simpdata.ML	Wed Oct 03 22:33:17 2007 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4    in case concl_of th of
     9.5           Const("Trueprop",_) $ P =>
     9.6              (case P of
     9.7 -                 Const("op :",_) $ a $ b => tryrules mem_pairs b
     9.8 +                 Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
     9.9                 | Const("True",_)         => []
    9.10                 | Const("False",_)        => []
    9.11                 | A => tryrules conn_pairs A)
    9.12 @@ -40,8 +40,8 @@
    9.13  (*Analyse a:b, where b is rigid*)
    9.14  val ZF_mem_pairs =
    9.15    [("Collect",  [CollectD1,CollectD2]),
    9.16 -   ("op -",     [DiffD1,DiffD2]),
    9.17 -   ("op Int",   [IntD1,IntD2])];
    9.18 +   (@{const_name Diff},     [DiffD1,DiffD2]),
    9.19 +   (@{const_name Int},   [IntD1,IntD2])];
    9.20  
    9.21  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    9.22