src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Dec 20 16:44:33 2010 +0100
@@ -29,7 +29,7 @@
 fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
 
 (*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
         error"Premises may not be conjuctive"
   | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
@@ -96,7 +96,7 @@
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = iT)
   in  case filter is_ind (args @ cs) of
-         [] => @{const 0}
+         [] => @{const zero}
        | u_args => Balanced_Tree.make mk_Un u_args
   end;