src/ZF/ind_syntax.ML
changeset 24826 78e6a3cea367
parent 23419 8c30dd4b3b22
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/ind_syntax.ML	Wed Oct 03 21:29:05 2007 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Wed Oct 03 22:33:17 2007 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  val iT = Type("i",[]);
     1.6  
     1.7 -val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
     1.8 +val mem_const = @{term mem};
     1.9  
    1.10  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    1.11  fun mk_all_imp (A,P) = 
    1.12 @@ -34,7 +34,7 @@
    1.13  
    1.14  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    1.15  
    1.16 -val apply_const = Const("op `", [iT,iT]--->iT);
    1.17 +val apply_const = @{term apply};
    1.18  
    1.19  val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    1.20  
    1.21 @@ -44,14 +44,14 @@
    1.22  (*simple error-checking in the premises of an inductive definition*)
    1.23  fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    1.24          error"Premises may not be conjuctive"
    1.25 -  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    1.26 +  | chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) = 
    1.27          (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
    1.28    | chk_prem rec_hd t = 
    1.29          (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
    1.30  
    1.31  (*Return the conclusion of a rule, of the form t:X*)
    1.32  fun rule_concl rl = 
    1.33 -    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
    1.34 +    let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) = 
    1.35                  Logic.strip_imp_concl rl
    1.36      in  (t,X)  end;
    1.37  
    1.38 @@ -74,7 +74,7 @@
    1.39  type constructor_spec = 
    1.40      ((string * typ * mixfix) * string * term list * term list);
    1.41  
    1.42 -fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    1.43 +fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
    1.44    | dest_mem _ = error "Constructor specifications must have the form x:A";
    1.45  
    1.46  (*read a constructor specification*)
    1.47 @@ -102,7 +102,7 @@
    1.48  
    1.49  fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
    1.50  
    1.51 -fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
    1.52 +fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
    1.53  
    1.54  val empty       = Const("0", iT)
    1.55  and univ        = Const("Univ.univ", iT-->iT)