src/ZF/ind_syntax.ML

 
 (** Abstract syntax definitions for ZF **)
 
 val iT = Type("i",[]);
 
-val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
+val mem_const = @{term mem};
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) = 
     FOLogic.all_const iT $ 
       Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
 	           Term.betapply(P, Bound 0));
 
 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
 
-val apply_const = Const("op `", [iT,iT]--->iT);
+val apply_const = @{term apply};
 
 val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
 
 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
         error"Premises may not be conjuctive"
-  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
+  | chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) = 
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
   | chk_prem rec_hd t = 
         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl = 
-    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
+    let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) = 
                 Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)
 fun rule_concl_msg sign rl = rule_concl rl

 (*Constructor name, type, mixfix info;
   internal name from mixfix, datatype sets, full premises*)
 type constructor_spec = 
     ((string * typ * mixfix) * string * term list * term list);
 
-fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
+fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
 fun read_construct sign (id, sprems, syn) =
     let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems

 	               $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
 
-fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
+fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
 
 val empty       = Const("0", iT)
 and univ        = Const("Univ.univ", iT-->iT)
 and quniv       = Const("QUniv.quniv", iT-->iT);