src/ZF/ind_syntax.ML

   let
     fun mk_intr ((id,T,syn), name, args, prems) =
       Logic.list_implies
         (map FOLogic.mk_Trueprop prems,
 	 FOLogic.mk_Trueprop
-	    (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
+	    (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
 	               $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);